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  6638  div2subap  8945  nn0addge1  9376  nn0addge2  9377  nn0sub2  9481  eluzp1p1  9709  uznn0sub  9715  iocssre  10110  icossre  10111  iccssre  10112  lincmb01cmp  10160  iccf1o  10161  fzosplitprm1  10400  subfzo0  10408  modfzo0difsn  10577  pfxpfx  11199  efltim  12124  fldivndvdslt  12363  prmdiv  12672  hashgcdlem  12675  vfermltl  12689  coprimeprodsq  12695  pythagtrip  12721  difsqpwdvds  12776  tgtop11  14663  sinq12gt0  15417  gausslemma2dlem1a  15650