Theorem biimpar 281

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

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  exbiri  364  bitr  441  eqtr  2057  opabss  3821  euotd  3991  wetriext  4301  sosng  4413  xpsspw  4450  brcogw  4504  funimaexglem  4982  funfni  4999  fnco  5007  fnssres  5012  fn0  5018  fnimadisj  5019  fnimaeq0  5020  foco  5116  foimacnv  5144  fvelimab  5229  fvopab3ig  5246  dff3im  5312  dffo4  5315  fmptco  5330  f1eqcocnv  5431  f1ocnv2d  5704  fnexALT  5740  xp1st  5792  xp2nd  5793  tfrlemiubacc  5944  tfri2d  5950  tfri3  5953  ecelqsg  6159  elqsn0m  6174  fidifsnen  6331  recclnq  6490  nq0a0  6555  qreccl  8576  difelfzle  8992  frec2uzlt2d  9190  caucvgrelemcau  9579  recvalap  9693  fzomaxdiflem  9708