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 )

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

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 1011

This theorem is referenced by:  nnawordex  6795  div2subap  9160  nn0addge1  9591  nn0addge2  9592  nn0sub2  9700  eluzp1p1  9930  uznn0sub  9936  iocssre  10337  icossre  10338  iccssre  10339  lincmb01cmp  10387  iccf1o  10389  fzosplitprm1  10634  subfzo0  10642  modfzo0difsn  10813  pfxpfx  11461  efltim  12446  fldivndvdslt  12685  prmdiv  12994  hashgcdlem  12997  vfermltl  13011  coprimeprodsq  13017  pythagtrip  13043  difsqpwdvds  13098  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemrv2  13246  tgtop11  15103  sinq12gt0  15857  gausslemma2dlem1a  16094  s2elclwwlknon2  16594