Theorem biimpa 324

Description: Inference from a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpd 135	. 2 |- (ph -> (ps -> ch))
3	2	imp 277	1 |- ((ph /\ ps) -> ch)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  pm5.1 501  euorv 1025  cgsex2g 1368  cgsex4g 1369  ceqsex 1370  sbcie 1455  limsssuc 2362  fnbr 2726  f1o00 2823  tz7.44lem1 2965  omordi 3164  th3qlem1 3250  en3d 3304  pw2en 3348  mapunen 3397  onomeneq 3414  r1ord 3499  rankr1 3518  nlt1pi 3827  indpi 3828  ltrpq 3879  addgt0sr 4007  divdivdivt 4265  leltnet 4287  addge0 4324  chocuni 5179  pjthlem10 5234  spanunsn 5482  3oalem2 5553  strlem5 5696  hatomistic 5755  cvexchlem 5759  atcvat3 5774  atcvat4 5775  mdsymlem1 5776  mdsymlem3 5778  mdsymlem5 5780

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org