Theorem biimp3a 1356

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 1196	1 |- ( ( ph /\ ps /\ ch ) -> th )

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

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 982

This theorem is referenced by:  nnawordex  6596  div2subap  8881  nn0addge1  9312  nn0addge2  9313  nn0sub2  9416  eluzp1p1  9644  uznn0sub  9650  iocssre  10045  icossre  10046  iccssre  10047  lincmb01cmp  10095  iccf1o  10096  fzosplitprm1  10327  subfzo0  10335  modfzo0difsn  10504  efltim  11880  fldivndvdslt  12119  prmdiv  12428  hashgcdlem  12431  vfermltl  12445  coprimeprodsq  12451  pythagtrip  12477  difsqpwdvds  12532  tgtop11  14396  sinq12gt0  15150  gausslemma2dlem1a  15383