Theorem biimp3a 1276

Description: Infer implication from a logical equivalence. Similar to biimpa 290. (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 290	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	2	3impa 1133	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  nnawordex  6124  nn0addge1  8334  nn0addge2  8335  nn0sub2  8421  eluzp1p1  8644  uznn0sub  8650  iocssre  8976  icossre  8977  iccssre  8978  lincmb01cmp  9025  iccf1o  9026  fzosplitprm1  9243  subfzo0  9251  modfzo0difsn  9397  fldivndvdslt  10335