Theorem biimp3a 919

Description: Infer implication from a logical equivalence. Similar to biimpa 416.

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 416	. 2 |- (((ph /\ ps) /\ ch) -> th)
3	2	3impa 828	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 775

This theorem is referenced by:  nn0addge1t 6130  nn0addge2t 6131  nn0sub2t 6162  znn0sub2t 6179  shftf 6351  iccssret 6396  eluzp1p1t 6435  seqzm1 6549  absimlet 6870  ser1absdif 6930  bccmplt 6962  fsum1ps 7018  ser1cmp2lem 7176  cncff 7266  methausi 7881  ioo2bl 7912  tgioolem 7914  lmcvg 7932  nv1 8304  pilem1 8671  sinq12gt0t 8708  ghomfo 10391  ghomlin 10393  ghomid 10394  ghomgsg 10395

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain