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  5183  fnco  5191  fnssres  5196  fnimadisj  5203  foco  5279  f1ores  5300  foimacnv  5303  fvelimab  5370  dff3  5420  dffo4  5423  f1o2d  5727  ecelqsg  5979  elqsn0  5993  peano4nc  6150  ncspw1eu  6159  ce0addcnnul  6179  sbth  6206  dflec2  6210  ce0lenc1  6239  ncfin  6247