Theorem biimp3a 1382

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

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

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 1007

This theorem is referenced by:  nnawordex  6740  div2subap  9076  nn0addge1  9507  nn0addge2  9508  nn0sub2  9614  eluzp1p1  9843  uznn0sub  9849  iocssre  10249  icossre  10250  iccssre  10251  lincmb01cmp  10299  iccf1o  10301  fzosplitprm1  10543  subfzo0  10551  modfzo0difsn  10720  pfxpfx  11355  efltim  12339  fldivndvdslt  12578  prmdiv  12887  hashgcdlem  12890  vfermltl  12904  coprimeprodsq  12910  pythagtrip  12936  difsqpwdvds  12991  tgtop11  14887  sinq12gt0  15641  gausslemma2dlem1a  15877  s2elclwwlknon2  16377