Theorem biimp3a 1381

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

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

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 1006

This theorem is referenced by:  nnawordex  6700  div2subap  9020  nn0addge1  9451  nn0addge2  9452  nn0sub2  9556  eluzp1p1  9785  uznn0sub  9791  iocssre  10191  icossre  10192  iccssre  10193  lincmb01cmp  10241  iccf1o  10242  fzosplitprm1  10484  subfzo0  10492  modfzo0difsn  10661  pfxpfx  11296  efltim  12280  fldivndvdslt  12519  prmdiv  12828  hashgcdlem  12831  vfermltl  12845  coprimeprodsq  12851  pythagtrip  12877  difsqpwdvds  12932  tgtop11  14827  sinq12gt0  15581  gausslemma2dlem1a  15814  s2elclwwlknon2  16314