Theorem biimp3a 1340

Description: Infer implication from a logical equivalence. Similar to biimpa 294. (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 294	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	2	3impa 1189	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  nnawordex  6508  div2subap  8754  nn0addge1  9181  nn0addge2  9182  nn0sub2  9285  eluzp1p1  9512  uznn0sub  9518  iocssre  9910  icossre  9911  iccssre  9912  lincmb01cmp  9960  iccf1o  9961  fzosplitprm1  10190  subfzo0  10198  modfzo0difsn  10351  efltim  11661  fldivndvdslt  11894  prmdiv  12189  hashgcdlem  12192  vfermltl  12205  coprimeprodsq  12211  pythagtrip  12237  difsqpwdvds  12291  tgtop11  12870  sinq12gt0  13545