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  9169  nn0addge1  9613  nn0addge2  9614  nn0sub2  9722  eluzp1p1  9957  uznn0sub  9963  iocssre  10365  icossre  10366  iccssre  10367  lincmb01cmp  10415  iccf1o  10417  fzosplitprm1  10663  subfzo0  10671  modfzo0difsn  10845  pfxpfx  11494  efltim  12481  fldivndvdslt  12720  prmdiv  13033  hashgcdlem  13036  vfermltl  13050  coprimeprodsq  13056  pythagtrip  13082  difsqpwdvds  13137  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemrv2  13314  tgtop11  15226  sinq12gt0  15981  gausslemma2dlem1a  16275  s2elclwwlknon2  16775