Theorem 3impib 831

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 375	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 827	1 |- ((ph /\ ps /\ ch) -> th)

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

This theorem is referenced by:  dedth3h 2388  frc 2920  ordunel 3084  funbrfvbg 3757  ssimaexg 3769  omwordri 4203  3ecoptocl 4305  infm3 6054  supxrleub 6099  uzind 6205  seqzrn 6557  facwordit 6944  csbfsum 7027  fsumcom 7028  fsumrev 7029  fsummulc1 7033  clm4at 7090  iserzmulc1 7136  fsum0diag 7258  efaddlem24 7361  sin01bndlem2 7468  cos01bndlem2 7470  sin01gt0 7476  inopnt 7600  basis1t 7614  meteq0 7812  opnin 7869  iscms2lem4 7992  ablcom 8103  ipassi 8501  spwval 8659  sincosq1sgn 8704  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  efifolem4 8725  efifolem6 8727  shaddclt 9085  shmulclt 9087  shsubclt 9089  chlim 9104  pjspansnt 9500  adjt 9857  lnfnmult 9977  atordt 10315  atcvat2t 10316  cdj3 10368  oooeqim2 10476  set2elt 10545  filint 10562  cmppfd 10678  domcmpd 10679  codcmpd 10680  cmpida 10707  cmpidb 10708  ishomd 10718

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