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  6584  div2subap  8858  nn0addge1  9289  nn0addge2  9290  nn0sub2  9393  eluzp1p1  9621  uznn0sub  9627  iocssre  10022  icossre  10023  iccssre  10024  lincmb01cmp  10072  iccf1o  10073  fzosplitprm1  10304  subfzo0  10312  modfzo0difsn  10469  efltim  11844  fldivndvdslt  12079  prmdiv  12376  hashgcdlem  12379  vfermltl  12392  coprimeprodsq  12398  pythagtrip  12424  difsqpwdvds  12479  tgtop11  14255  sinq12gt0  15006  gausslemma2dlem1a  15215