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  6587  div2subap  8864  nn0addge1  9295  nn0addge2  9296  nn0sub2  9399  eluzp1p1  9627  uznn0sub  9633  iocssre  10028  icossre  10029  iccssre  10030  lincmb01cmp  10078  iccf1o  10079  fzosplitprm1  10310  subfzo0  10318  modfzo0difsn  10487  efltim  11863  fldivndvdslt  12102  prmdiv  12403  hashgcdlem  12406  vfermltl  12420  coprimeprodsq  12426  pythagtrip  12452  difsqpwdvds  12507  tgtop11  14312  sinq12gt0  15066  gausslemma2dlem1a  15299