Theorem biimp3a 921

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

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

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

This theorem is referenced by:  nn0addge1t 6132  nn0addge2t 6133  nn0sub2t 6164  znn0sub2t 6181  shftf 6352  iccssret 6397  eluzp1p1t 6436  seqzm1 6550  absimlet 6870  ser1absdif 6930  bccmplt 6962  fsum1ps 7018  ser1cmp2lem 7176  cncff 7266  methausi 7878  ioo2bl 7909  tgioolem 7911  lmcvg 7929  nv1 8300  pilem1 8666  sinq12gt0t 8703  ghomfo 10386  ghomlin 10388  ghomid 10389  ghomgsg 10390

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 779

Copyright terms: Public domain