Theorem biimpar 471

Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

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 214	. 2 |- (ph -> (ch -> ps))
3	2	imp 418	1 |- ((ph /\ ch) -> ps)

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  exbiri  605  bitr  689  oplem1  930  eqtr  2370  funfni  5184  fnco  5192  fnssres  5197  fnimadisj  5204  foco  5280  f1ores  5301  foimacnv  5304  fvelimab  5371  dff3  5421  dffo4  5424  f1o2d  5728  ecelqsg  5980  elqsn0  5994  peano4nc  6151  ncspw1eu  6160  ce0addcnnul  6180  sbth  6207  dflec2  6211  ce0lenc1  6240  ncfin  6248