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  6807  div2subap  9175  nn0addge1  9620  nn0addge2  9621  nn0sub2  9727  eluzp1p1  9963  uznn0sub  9969  iocssre  10371  icossre  10372  iccssre  10373  lincmb01cmp  10421  iccf1o  10423  fzosplitprm1  10669  subfzo0  10677  modfzo0difsn  10852  pfxpfx  11501  efltim  12489  fldivndvdslt  12728  prmdiv  13041  hashgcdlem  13044  vfermltl  13058  coprimeprodsq  13064  pythagtrip  13090  difsqpwdvds  13145  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemrv2  13322  tgtop11  15319  sinq12gt0  16074  gausslemma2dlem1a  16399  s2elclwwlknon2  16899