Theorem biimp3a 1386

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  nnawordex  6806  div2subap  9175  nn0addge1  9620  nn0addge2  9621  nn0sub2  9729  eluzp1p1  9964  uznn0sub  9970  iocssre  10372  icossre  10373  iccssre  10374  lincmb01cmp  10422  iccf1o  10424  fzosplitprm1  10670  subfzo0  10678  modfzo0difsn  10853  pfxpfx  11502  efltim  12490  fldivndvdslt  12729  prmdiv  13042  hashgcdlem  13045  vfermltl  13059  coprimeprodsq  13065  pythagtrip  13091  difsqpwdvds  13146  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemrv2  13323  tgtop11  15302  sinq12gt0  16057  gausslemma2dlem1a  16382  s2elclwwlknon2  16882