Theorem 3impb 1063

Description: Importation from double to triple conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
2	1	exp32 408	. 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:  3adant1l 1090  3adant1r 1091  syl3an1 1130  3impdi 1152  rcla42ev 2385  reuss 2871  wereu 3654  funtp 4468  resdif 4659  fnotoprb 4916  foprrn 4965  fnoprvrn 4968  odi 5258  oeoa 5272  oeoe 5274  ecopoprtrn 5370  ecoprass 5379  ecoprdi 5380  supmaxlem 5678  addasspi 6175  mulasspi 6177  distrpi 6178  ltapq 6228  ltmpq 6229  genpass 6264  distrpr 6284  ltapr 6303  cnegexlem1 6499  addsub 6542  subdi 6590  submul2 6625  subsub2 6626  pnpcan 6645  xrlttr 6728  le2tri3i 6764  ltaddsub 6814  leaddsub 6816  divne0b 6911  div12 6927  diveq0 6944  divneg 6950  divdiv2 6973  lble 7256  uzind3 7419  qdivcl 7454  irrmul 7458  modcyc 7516  modcyc2 7517  fzen 7664  lenegsq 8137  faclbnd4lem4 8203  fsummulc2 8294  clm0ii 8349  clim2serz 8394  iserzcmp0 8403  isummulc1iALT 8474  geoisum1c 8507  fsum0diag2 8521  uncld 8957  ntrss 8964  innei 9012  sncld 9064  blin 9129  ssbl 9132  opni2 9142  bl2ioo 9189  lmss 9231  bcthlem7 9283  bcthlem9 9285  grpsn 9340  grpinvid1 9356  grpinvid2 9357  gxval 9381  abl4 9413  ablnncan 9420  issubg 9425  issubgi 9431  ablmul 9439  ghgrpilem4 9444  isga 9450  vcnegsubdi2 9526  nvnpcan 9612  nvmeq0 9616  nvabs 9633  lnocoi 9757  nmorepnf 9770  blo3i 9802  blometi 9803  ipasslem5 9835  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  laspwcl 10011  lanfwcl 10012  symggrpi 10205  hvmulcan 10571  hvmulcanOLD 10572  his5 10586  his7 10589  his2sub2 10592  hhssnv 10767  pjeq2 10874  homcl 11157  fh1 11194  fh2 11195  cm2j 11196  homco1 11364  homulass 11365  hoadddi 11366  hosubsub2 11375  braadd 11506  bramul 11507  kbmul 11516  lnopmul 11528  lnopli 11529  lnopaddmuli 11534  lnopsubmuli 11536  homco2 11538  lnfnli 11606  lnfnaddmuli 11611  kbass2 11688  mdexchi 11907  bnj565 12543  bnj566 12544  bnj1065 12901  bnj229 13253  bnj518 13260  bnj546 13272  bnj1066 13398  fnn0ind 13611  fseq1cl 13619  cayleylem2 13642  dvds0lem 13665  dvdscmulr 13682  dvdsmulcr 13683  dvds2add 13685  dvds2sub 13686  dvdsleabs 13694  divalg 13706  divalgb 13707  ndvdsadd 13711  gcdcllem3 13720  dvdslegcd 13723  modgcd 13738  algrp1lem 13741  mulgcdlem7 13762  absmulgcd 13764  dvdsgcd 13765  ficli 14353  finminlem 15367  elfiun 15369  subsubtop 15423  ivthALT 15454  unopn 15835  subspabs 15840  lpss2 15842  geomcau 15849  txcnoprab 15911  rrnmval 16014  exidcl 16029  pcorev 16087  elpi1i 16090  pi1val 16094  ringneglmul 16104  ringnegrmul 16105  divrngcl 16110  crngcom 16149  crngm4 16151  inidl 16178  pltval 16781  pgeval 16794  joinval 16815  joinval2 16816  meetval 16822  meetval2 16823  lubel 16898  oposlem 16913  hlsuprexch 17033  grpclNEW 17106  grpinvid1NEW 17131  grpinvid2NEW 17132  ringclNEW 17144  plusssval 17205

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