Theorem biimp3a 1358

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

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

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 983

This theorem is referenced by:  nnawordex  6617  div2subap  8912  nn0addge1  9343  nn0addge2  9344  nn0sub2  9448  eluzp1p1  9676  uznn0sub  9682  iocssre  10077  icossre  10078  iccssre  10079  lincmb01cmp  10127  iccf1o  10128  fzosplitprm1  10365  subfzo0  10373  modfzo0difsn  10542  efltim  12042  fldivndvdslt  12281  prmdiv  12590  hashgcdlem  12593  vfermltl  12607  coprimeprodsq  12613  pythagtrip  12639  difsqpwdvds  12694  tgtop11  14581  sinq12gt0  15335  gausslemma2dlem1a  15568