Theorem biimp3a 1324

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  nnawordex  6432  div2subap  8620  nn0addge1  9047  nn0addge2  9048  nn0sub2  9148  eluzp1p1  9375  uznn0sub  9381  iocssre  9766  icossre  9767  iccssre  9768  lincmb01cmp  9816  iccf1o  9817  fzosplitprm1  10042  subfzo0  10050  modfzo0difsn  10199  efltim  11441  fldivndvdslt  11668  hashgcdlem  11939  tgtop11  12284  sinq12gt0  12959