Theorem biimp3a 1358

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

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

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 983

This theorem is referenced by:  nnawordex  6615  div2subap  8910  nn0addge1  9341  nn0addge2  9342  nn0sub2  9446  eluzp1p1  9674  uznn0sub  9680  iocssre  10075  icossre  10076  iccssre  10077  lincmb01cmp  10125  iccf1o  10126  fzosplitprm1  10363  subfzo0  10371  modfzo0difsn  10540  efltim  12009  fldivndvdslt  12248  prmdiv  12557  hashgcdlem  12560  vfermltl  12574  coprimeprodsq  12580  pythagtrip  12606  difsqpwdvds  12661  tgtop11  14548  sinq12gt0  15302  gausslemma2dlem1a  15535