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  6802  div2subap  9167  nn0addge1  9609  nn0addge2  9610  nn0sub2  9718  eluzp1p1  9948  uznn0sub  9954  iocssre  10355  icossre  10356  iccssre  10357  lincmb01cmp  10405  iccf1o  10407  fzosplitprm1  10653  subfzo0  10661  modfzo0difsn  10832  pfxpfx  11480  efltim  12465  fldivndvdslt  12704  prmdiv  13013  hashgcdlem  13016  vfermltl  13030  coprimeprodsq  13036  pythagtrip  13062  difsqpwdvds  13117  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemrv2  13265  tgtop11  15177  sinq12gt0  15931  gausslemma2dlem1a  16177  s2elclwwlknon2  16677