Theorem biimp3ar 1433

Description: Infer implication from a logical equivalence. Similar to biimpar 502. (Contributed by NM, 2-Jan-2009.)

Hypothesis

Ref	Expression
biimp3a.1	|- ( ( ph /\ ps ) -> ( ch <-> th ) )

Assertion

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

Proof of Theorem biimp3ar

Step	Hyp	Ref	Expression
1		biimp3a.1	. . 3 |- ( ( ph /\ ps ) -> ( ch <-> th ) )
2	1	exbiri 652	. 2 |- ( ph -> ( ps -> ( th -> ch ) ) )
3	2	3imp 1256	1 |- ( ( ph /\ ps /\ th ) -> ch )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  rmoi  3530  brelrng  5355  div2sub  10850  nn0p1elfzo  12510  ssfzo12  12561  modltm1p1mod  12722  abssubge0  14067  qredeu  15372  abvne0  18827  slesolinvbi  20487  basgen2  20793  fcfval  21837  nmne0  22423  ovolfsf  23240  lgssq  25062  lgssq2  25063  colinearalg  25790  usgr0v  26133  frgr0vb  27126  nv1  27530  adjeq  28794  areacirc  33505  fvopabf4g  33515  exidreslem  33676  hgmapvvlem3  37217  iocmbl  37798  iunconnlem2  39171  ssfz12  41324  m1modmmod  42316