MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3exp2 Structured version   Visualization version   GIF version

Theorem 3exp2 1355
Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3exp2.1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
3exp2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem 3exp2
StepHypRef Expression
1 3exp2.1 . . 3 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
21ex 414 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
323expd 1354 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090
This theorem is referenced by:  3anassrs  1361  pm2.61da3ne  3035  po2nr  5564  fliftfund  7263  frfi  9239  fin33i  10312  axdc3lem4  10396  iscatd  17560  isfuncd  17758  isposd  18219  pospropd  18223  imasmnd2  18600  grpinveu  18792  grpid  18793  grpasscan1  18817  imasgrp2  18869  dmdprdd  19785  pgpfac1lem5  19865  imasring  20052  islmodd  20344  lmodvsghm  20399  islssd  20412  islmhm2  20515  mulgghm2  20913  isphld  21074  psrbaglefiOLD  21351  riinopn  22273  ordtbaslem  22555  subbascn  22621  haust1  22719  isnrm2  22725  isnrm3  22726  lmmo  22747  nllyidm  22856  tx1stc  23017  filin  23221  filtop  23222  isfil2  23223  infil  23230  fgfil  23242  isufil2  23275  ufileu  23286  filufint  23287  flimopn  23342  flimrest  23350  isxmetd  23695  met2ndc  23895  icccmplem2  24202  lmmbr  24638  cfil3i  24649  equivcfil  24679  bcthlem5  24708  volfiniun  24927  dvidlem  25295  ulmdvlem3  25777  ax5seg  27929  axcontlem4  27958  axcont  27967  grporcan  29502  grpoinveu  29503  grpoid  29504  cvxpconn  33876  cvxsconn  33877  mclsax  34203  mclsppslem  34217  broutsideof2  34736  nn0prpwlem  34823  fgmin  34871  poimirlem27  36134  poimirlem29  36136  poimirlem31  36138  cntotbnd  36284  heiborlem6  36304  heiborlem10  36308  rngonegmn1l  36429  rngonegmn1r  36430  rngoneglmul  36431  rngonegrmul  36432  crngm23  36490  prnc  36555  pridlc3  36561  dmncan1  36564  lsmsat  37499  eqlkr  37590  llncmp  38014  2at0mat0  38017  llncvrlpln  38050  lplncmp  38054  lplnexllnN  38056  lplncvrlvol  38108  lvolcmp  38109  linepsubN  38244  pmapsub  38260  paddasslem16  38327  pmodlem2  38339  lhp2lt  38493  ltrneq2  38640  cdlemf2  39054  cdlemk34  39402  cdlemn11pre  39702  dihord2pre  39717  onexoegt  41607
  Copyright terms: Public domain W3C validator