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  6764  div2subap  9113  nn0addge1  9544  nn0addge2  9545  nn0sub2  9653  eluzp1p1  9883  uznn0sub  9889  iocssre  10289  icossre  10290  iccssre  10291  lincmb01cmp  10339  iccf1o  10341  fzosplitprm1  10584  subfzo0  10592  modfzo0difsn  10761  pfxpfx  11404  efltim  12388  fldivndvdslt  12627  prmdiv  12936  hashgcdlem  12939  vfermltl  12953  coprimeprodsq  12959  pythagtrip  12985  difsqpwdvds  13040  ballotfilemfc0  13153  ballotfilemfcc  13154  tgtop11  14958  sinq12gt0  15712  gausslemma2dlem1a  15948  s2elclwwlknon2  16448