Theorem biimp3a 1355

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

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

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 981

This theorem is referenced by:  nnawordex  6543  div2subap  8807  nn0addge1  9235  nn0addge2  9236  nn0sub2  9339  eluzp1p1  9566  uznn0sub  9572  iocssre  9966  icossre  9967  iccssre  9968  lincmb01cmp  10016  iccf1o  10017  fzosplitprm1  10247  subfzo0  10255  modfzo0difsn  10408  efltim  11719  fldivndvdslt  11953  prmdiv  12248  hashgcdlem  12251  vfermltl  12264  coprimeprodsq  12270  pythagtrip  12296  difsqpwdvds  12350  tgtop11  13847  sinq12gt0  14522