Theorem biimp3a 1356

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

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

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 982

This theorem is referenced by:  nnawordex  6589  div2subap  8867  nn0addge1  9298  nn0addge2  9299  nn0sub2  9402  eluzp1p1  9630  uznn0sub  9636  iocssre  10031  icossre  10032  iccssre  10033  lincmb01cmp  10081  iccf1o  10082  fzosplitprm1  10313  subfzo0  10321  modfzo0difsn  10490  efltim  11866  fldivndvdslt  12105  prmdiv  12414  hashgcdlem  12417  vfermltl  12431  coprimeprodsq  12437  pythagtrip  12463  difsqpwdvds  12518  tgtop11  14338  sinq12gt0  15092  gausslemma2dlem1a  15325