Theorem biimp3a 1382

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

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

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 1007

This theorem is referenced by:  nnawordex  6775  div2subap  9131  nn0addge1  9562  nn0addge2  9563  nn0sub2  9671  eluzp1p1  9901  uznn0sub  9907  iocssre  10308  icossre  10309  iccssre  10310  lincmb01cmp  10358  iccf1o  10360  fzosplitprm1  10605  subfzo0  10613  modfzo0difsn  10784  pfxpfx  11428  efltim  12412  fldivndvdslt  12651  prmdiv  12960  hashgcdlem  12963  vfermltl  12977  coprimeprodsq  12983  pythagtrip  13009  difsqpwdvds  13064  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemrv2  13212  tgtop11  15070  sinq12gt0  15824  gausslemma2dlem1a  16060  s2elclwwlknon2  16560