Theorem 3impb 835

Description: Importation from double to triple conjunction.

Hypothesis

Ref	Expression
3impb.1	⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)

Assertion

Ref	Expression
3impb	⊢ ((φ ⋀ ψ ⋀ χ) → θ)

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 ⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)
2	1	exp32 377	. 2 ⊢ (φ → (ψ → (χ → θ)))
3	2	3imp 833	1 ⊢ ((φ ⋀ ψ ⋀ χ) → θ)

Syntax hints:   → wi 3   ⋀ wa 221   ⋀ w3a 781

This theorem is referenced by:  3adant1l 858  3adant1r 859  syl3an1 865  3impdi 886  rcla42ev 1927  reuss 2328  wereu 2972  resdif 3816  fnotoprb 4049  foprrn 4096  fnoprvrn 4099  odi 4346  oeoa 4360  oeoe 4362  ecopoprtrn 4452  ecoprass 4461  ecoprdi 4462  supmaxlem 4731  addasspi 5177  mulasspi 5179  distrpi 5180  ltapq 5230  ltmpq 5231  genpass 5266  distrpr 5286  ltapr 5305  cnegexlem1 5499  subdi 5581  submul2 5614  subsub2 5615  pnpcan 5632  xrlttr 5707  le2tri3i 5743  ltaddsub 5785  leaddsub 5787  divne0b 5874  div12 5890  diveq0 5907  divneg 5913  divdiv2 5935  lble 6215  uzind3 6378  qdivcl 6413  irrmul 6417  modcyc 6475  modcyc2 6476  fzen 6622  lenegsq 7088  faclbnd4lem4 7154  fsummulc2 7237  clm0ii 7292  clim2serz 7337  iserzcmp0 7346  isummulc1iALT 7417  geoisum1c 7450  fsum0diag2 7464  reeftlcl 7585  uncld 7891  ntrss 7898  innei 7946  sncld 7997  blin 8062  ssbl 8065  opni2 8075  cncfmet 8116  bl2ioo 8122  lmss 8164  bcthlem7 8216  bcthlem9 8218  grpsn 8273  grpinvid1 8289  grpinvid2 8290  gxval 8314  abl4 8346  ablnncan 8353  issubg 8358  issubgi 8364  ablmul 8372  ghgrpilem4 8377  vcnegsubdi2 8441  nvnpcan 8527  nvmeq0 8531  nvabs 8548  lnocoi 8672  nmorepnf 8685  blo3i 8717  blometi 8718  ipasslem5 8750  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  laspwcl 8930  lanfwcl 8931  hvmulcan 9214  hvmulcanOLD 9215  his5 9229  his7 9232  his2sub2 9235  hhssnv 9410  pjeq2 9517  homcl 9800  fh1 9837  fh2 9838  cm2j 9839  homco1 10007  homulass 10008  hoadddi 10009  hosubsub2 10018  braadd 10149  bramul 10150  kbmul 10159  lnopmul 10170  lnopli 10171  lnopaddmuli 10176  lnopsubmuli 10178  homco2 10180  lnfnli 10248  lnfnaddmuli 10253  kbass2 10330  mdexchi 10543  symggrpi 10691  cayleylem2 10695  ficli 10756  finminlem 11418  elfiun 11421  subsubtop 11479  ivthALT 11515  isga 11772  unopn 11898  subspabs 11903  lpss2 11906  geomcau 11914  txcnoprab 11981  rrnmval 12070

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