Theorem biimpar 417

Description: Inference from a logical equivalence.

Hypothesis

Ref	Expression
biimpa.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biimpar	|- ((ph /\ ch) -> ps)

Proof of Theorem biimpar

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimprd 154	. 2 |- (ph -> (ch -> ps))
3	2	imp 350	1 |- ((ph /\ ch) -> ps)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm4.22 622  oplem1 772  eqtrt 1492  hbsbc1gd 1983  hbsbcgd 1984  ifboth 2375  opabss 2668  sotrieq 2861  ssrel 3247  funfni 3588  fnco 3595  fnssres 3600  funimadisj 3606  fnex 3607  foco 3682  f1ores 3703  fvopab3ig 3778  dff2 3817  dffo4 3820  abrexexlem1 3858  isomin 3899  tfrlem1 3911  tfr3 3926  oprabvalig 4024  oawordri 4184  oaass 4195  en3d 4401  aceq5 4740  ltexprlem7 5148  pm2.61ltle 5534  uzindOLD 6208  btwnzge0t 6245  eluzfzt 6477  elfz1eqt 6492  fznn0sub2t 6499  expgt1t 6592  abssubge0t 6895  faclbnd4lem4 6951  fsumsplit 7020  serz1p 7052  serzcmp0 7055  climconst 7094  climcmpc1 7139  ser1f0 7170  isumclim3t 7200  isumclim5t 7202  geoisumr 7243  mulc1cncf 7279  uniopnt 7598  basgen2t 7639  bastop 7642  clsval 7677  neival 7717  lpval 7743  cnsscnp 7772  cncnplem2 7775  bl2in 7843  blss 7853  neibl 7877  lpbl 7880  metcnpf 7883  metcnconst 7885  metcnp 7887  tgioolem 7914  lmfexlem3 7958  metelcls 7965  metcld 7967  metcn4 7971  cmsss 7997  bcthlem29 8027  resgrprn 8095  issubg 8116  nv1 8304  sspn 8395  nmblolbii 8459  blocnilem 8464  blocni 8465  ubthlem7 8535  ubthlem8 8536  ubthlem10 8538  sineq0 8713  efifolem7 8728  efif1lem1 8730  efif1lem2 8731  norm1t 9121  norm1ex 9122  occllem6 9178  normcant 9499  pjoi0t 9662  adjeqt 9859  eighmortht 9888  nmbdoplb 9949  nmcoplb 9958  nmophm 9961  nmbdfnlb 9978  nmcfnlb 9987  riesz3 9995  cnlnadjlem7 10006  branmfnt 10038  nmopleidt 10072  hstlet 10157  superpos 10281  cvexchlem 10295  cmpmorp 10712

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain