Theorem 3impia 1064

Description: Importation to triple conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 |- ((ph /\ ps) -> (ch -> th))
2	1	ex 402	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 1061	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  mopick2 1837  3gencl 2320  vtoclegftOLD 2357  disjne 2919  disjneOLD 2920  opthgg 3534  tz7.2 3639  ndmoprg 4976  oaass 5243  oeoalem 5271  oeoelem 5273  xpdom1g 5503  unidomg 5971  cdaung 6071  cdaeng 6074  axsup 6676  ltne 6686  xrltne 6740  divcl 6901  divcan1 6909  divrec 6922  divcan3 6938  redivcl 6978  letrp1 6994  p1le 6995  zextle 7401  zextlt 7402  btwnnz 7404  gtndiv 7405  uzind2 7418  qbtwnre 7459  qbtwnxr 7460  flwordi 7477  ceile 7491  modadd1 7518  modmul1 7519  modirr 7522  iccleub 7551  snunioo 7584  elfz4 7645  expge1 7835  exprec 7837  exple1 7852  absdiv 8111  cjdiv 8141  bccl2 8223  fsum1ps 8278  iserzex 8395  isumrecl 8471  explecnv 8495  cncffvelrnOLD 8529  ivthlem6 8548  ivthlem7 8549  znnenlem 8770  clsndisj 8982  metcni 9172  lmfss 9226  lmcl 9227  bcthlem8 9284  bcth 9310  grpasscan1 9361  gxnn0neg 9386  gxnn0suc 9387  gxcl 9388  gxneg 9389  gxcom 9392  gxinv 9393  gxsuc 9395  gxnn0add 9397  gxadd 9398  gxnn0mul 9400  gxmul 9401  grplactf1o 9406  gxdi 9422  gagrpid 9458  gaass 9459  nvs 9622  nvtri 9630  nmlno0 9795  nmlnoubi 9796  hlipgt0 9963  spwnex 10004  sincosq1lem 10052  efifolem4 10079  efifolem5 10080  sfseqeq 10169  dif1enOLD 10173  fipreima 10175  hausnei2 10222  fbssint 10279  limfilss 10299  flimnei 10301  comptoppr 10332  ocnel 10803  elspansn2 11123  elspansn3 11128  normcan 11132  pjoml2 11187  lecm 11193  osum 11223  nmbdfnlb 11616  leopmul 11705  hstpyth 11801  cvnbtwn 11858  ssmd1 11883  ssmd2 11884  ssdmd1 11885  ssdmd2 11886  cvmd 11908  cvdmd 11909  superpos 11926  bnj1140 12938  fzind 13610  cayleylem2 13642  suprzcl 13658  dvdsle 13693  divalgb 13707  ndvdssub 13710  algcvga 13747  mulgcdlem2 13757  poseq 13954  axdenselem8 14026  jop 14532  mop 14533  labs1 14536  labs2 14538  valcurfn 14551  supdef 14604  mgmlion 14697  fprodneg 14741  imtr 14762  intfmu2 14867  cnvhmphb 14880  conttnf 14944  bwt2 14960  trhom2 14985  dmse1 15001  mslb1 15007  2wsms 15008  lvsovso 15038  cmpassoh 15150  cmpmon 15164  icmpmon 15165  tarax3b 15223  tarax3e 15228  isseg2 15305  hmeoclda 15421  hmeocldb 15422  compcov 15429  hscptsscld 15434  compfipin0lem 15435  alexsub 15441  conntoppr 15445  fnessex 15484  fneuni 15485  refssex 15490  locfinnei 15512  ufilen 15579  fclusneii 15609  fclsfnflim 15614  fvopabf4g 15703  erthdmg 15730  fipreimaOLD 15756  inficl 15757  eluzsub 15783  seq1p1g 15805  seqz1g 15806  seqzp1g 15807  incsequz 15815  iserzshft2 15829  subspcld2 15839  iccsplit 15854  iimulcl 15874  paste 15893  ismtybndlem 15952  ismtybnd 15953  heiborlem13 15967  bfp 16009  rngisocnv 16135  risci 16141  ordintdif 16440  smoel 16451  joinle 16820  meetle 16827  clatglble 16902  omlfh3 16979  cvrnbtwn 16990  cvrnbtwn2 16992  cvrnbtwn4 16996  hlexch3 17041  hlexch4 17042  hlatexchb1 17043  atcvrj0 17065  psubat 17235  pmapglb2 17253  pmapglb2x 17254  paddasslem17 17297  pmod2i 17310  pmodl42 17312  osumcllem8 17371  pexmidlem3 17380  pl42lem1 17407  pl42lem4 17410

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 164  df-an 242  df-3an 860

Copyright terms: Public domain