Theorem 3impib 837

Description: Importation to triple conjunction.

Hypothesis

Ref	Expression
3impib.1	|- (ph -> ((ps /\ ch) -> th))

Assertion

Ref	Expression
3impib	|- ((ph /\ ps /\ ch) -> th)

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 |- (ph -> ((ps /\ ch) -> th))
2	1	exp3a 374	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 833	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 221   /\ w3a 781

This theorem is referenced by:  dedth3h 2442  frc 2950  ordunel 3181  funbrfvbg 3868  ssimaexg 3880  omwordri 4339  3ecoptocl 4446  infm3 6222  supxrleub 6267  uzind 6376  seqzrn 6752  facwordi 7147  csbfsum 7230  fsumcom 7231  fsumrev 7232  fsummulc1 7236  clm4a 7293  iserzmulc1 7339  fsum0diag 7463  efaddlem24 7566  sin01bndlem2 7677  cos01bndlem2 7679  sin01gt0 7685  inopn 7812  basis1 7826  meteq0 8022  opnin 8079  iscms2lem4 8203  ablcom 8344  vacnlem3 8584  ipassi 8757  spwval 8921  sincosq1sgn 8971  sincosq2sgn 8972  sincosq3sgn 8973  sincosq4sgn 8974  efifolem4 8997  efifolem6 8999  shaddcl 9361  shmulcl 9363  shsubcl 9365  chlimi 9380  pjspansn 9776  adj1 10137  lnfnmul 10256  atord 10597  atcvat2 10598  cdj3i 10650  oooeqim2 10759  set2elt 10827  filint 11075  cmppfd 11199  domcmpd 11200  codcmpd 11201  cmpida 11228  cmpidb 11229  ishomd 11245  ordtypelem1 11427  fbasssin 11625  filfinnfr 11646  hausfillim 11685  dirge 11754  fimaxg 11838  acdcg 11842  acdc3g 11843  acdc5g 11844  indexf 11847  elnnr 11874

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 145  df-an 223  df-3an 783

Copyright terms: Public domain