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 621  oplem1 771  eqtrt 1489  hbsbc1gd 1979  hbsbcgd 1980  ifboth 2371  opabss 2663  sotrieq 2856  ssrel 3242  funfni 3580  fnco 3587  fnssres 3592  funimadisj 3598  fnex 3599  foco 3673  f1ores 3694  fvopab3ig 3769  dff2 3808  dffo4 3811  abrexexlem1 3849  isomin 3890  tfrlem1 3902  tfr3 3917  oprabvalig 4015  oawordri 4174  oaass 4185  en3d 4388  aceq5 4720  ltexprlem7 5128  pm2.61ltle 5515  uzindOLD 6164  btwnzge0t 6196  eluzfzt 6417  elfz1eqt 6432  fznn0sub2t 6439  expgt1t 6531  abssubge0t 6841  faclbnd4lem4 6896  fsumsplit 6966  serz1p 6998  serzcmp0 7001  climconst 7039  climcmpc1 7083  ser1f0 7114  isumclim3t 7143  isumclim5t 7145  geoisumr 7186  mulc1cncf 7222  uniopnt 7548  basgen2t 7589  bastop 7592  clsval 7627  neival 7667  lpval 7693  cnsscnp 7722  cncnplem2 7725  bl2in 7795  blss 7805  neibl 7829  lpbl 7832  metcnpf 7835  metcnconst 7837  metcnp 7839  tgioolem 7866  lmfexlem3 7909  metelcls 7916  metcld 7917  metcn4 7921  cmsss 7947  bcthlem29 7977  resgrprn 8045  issubg 8068  nv1 8256  sspn 8342  nmblolbii 8403  blocnilem 8408  blocni 8409  ubthlem7 8479  ubthlem8 8480  ubthlem10 8482  efifolem7 8662  efif1lem1 8664  efif1lem2 8665  norm1t 9060  norm1ex 9061  occllem6 9117  normcant 9439  pjoi0t 9602  adjeqt 9798  eighmortht 9827  nmbdoplb 9887  nmcoplb 9896  nmophm 9899  nmbdfnlb 9916  nmcfnlb 9925  riesz3 9933  cnlnadjlem7 9944  branmfnt 9976  nmopleidt 10010  hstlet 10095  superpos 10218  cvexchlem 10232  cmpmorp 10592

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