Theorem biimp3a 1379

Description: Infer implication from a logical equivalence. Similar to biimpa 296. (Contributed by NM, 4-Sep-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem biimp3a

Step	Hyp	Ref	Expression
1		biimp3a.1	. . 3 |- ( ( ph /\ ps ) -> ( ch <-> th ) )
2	1	biimpa 296	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	2	3impa 1218	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  nnawordex  6675  div2subap  8984  nn0addge1  9415  nn0addge2  9416  nn0sub2  9520  eluzp1p1  9748  uznn0sub  9754  iocssre  10149  icossre  10150  iccssre  10151  lincmb01cmp  10199  iccf1o  10200  fzosplitprm1  10440  subfzo0  10448  modfzo0difsn  10617  pfxpfx  11240  efltim  12209  fldivndvdslt  12448  prmdiv  12757  hashgcdlem  12760  vfermltl  12774  coprimeprodsq  12780  pythagtrip  12806  difsqpwdvds  12861  tgtop11  14750  sinq12gt0  15504  gausslemma2dlem1a  15737