Theorem biimp3a 1335

Description: Infer implication from a logical equivalence. Similar to biimpa 294. (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 294	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	2	3impa 1184	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  nnawordex  6492  div2subap  8729  nn0addge1  9156  nn0addge2  9157  nn0sub2  9260  eluzp1p1  9487  uznn0sub  9493  iocssre  9885  icossre  9886  iccssre  9887  lincmb01cmp  9935  iccf1o  9936  fzosplitprm1  10165  subfzo0  10173  modfzo0difsn  10326  efltim  11635  fldivndvdslt  11868  prmdiv  12163  hashgcdlem  12166  vfermltl  12179  coprimeprodsq  12185  pythagtrip  12211  difsqpwdvds  12265  tgtop11  12676  sinq12gt0  13351