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

Theorem 3impa 1251
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impa.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
3impa ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21exp31 628 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1249 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  ex3  1255  3impdir  1374  syl3an9b  1389  biimp3a  1424  stoic3  1692  rspec3  2919  rspc3v  3296  raltpg  4183  rextpg  4184  disjiun  4568  otthg  4874  3optocl  5110  fun2ssres  5831  funtpg  5842  funssfv  6104  foco2OLD  6273  f1elima  6399  ot1stg  7051  ot2ndg  7052  smogt  7329  omord2  7512  omword  7515  oeword  7535  omabslem  7591  ecovass  7720  fpmg  7747  findcard  8062  cdaun  8855  cfsmolem  8953  ingru  9494  addasspi  9574  mulasspi  9576  ltapi  9582  ltmpi  9583  axpre-ltadd  9845  leltne  9979  dedekind  10052  recextlem2  10510  divdiv32  10585  divdiv1  10588  lble  10827  fnn0ind  11311  supminf  11610  xrleltne  11816  xrmaxeq  11846  xrmineq  11847  iccgelb  12060  elicc4  12070  iccsplit  12135  elfz  12161  fzrevral  12252  modabs  12523  expgt0  12713  expge0  12716  expge1  12717  mulexpz  12720  expp1z  12729  expm1  12730  digit1  12818  faclbnd4  12904  faclbnd5  12905  abssubne0  13853  binom  14350  dvds0lem  14779  dvdsnegb  14786  muldvds1  14793  muldvds2  14794  dvdscmulr  14797  dvdsmulcr  14798  divalgmodcl  14918  gcd2n0cl  15018  gcdaddm  15033  lcmdvds  15108  prmdvdsexp  15214  rpexp1i  15220  monpropd  16169  prfval  16611  xpcpropd  16620  curf2ndf  16659  eqglact  17417  mndodcongi  17734  oddvdsnn0  17735  efgi0  17905  efgi1  17906  lss0cl  18717  scmatscmid  20079  pmatcollpw3fi1lem1  20358  cnpval  20798  cnf2  20811  cnnei  20844  lfinun  21086  ptpjcn  21172  cnmptk2  21247  flfval  21552  cnmpt2plusg  21650  cnmpt2vsca  21756  ustincl  21769  xbln0  21977  blssec  21998  blpnfctr  21999  mopni2  22056  mopni3  22057  nmoval  22277  nmocl  22282  isnghm2  22286  isnmhm2  22314  cnmpt2ds  22402  metdseq0  22413  cnmpt2ip  22800  caucfil  22834  mbfimasn  23152  dvnf  23441  dvnbss  23442  coemul  23757  dvply1  23788  dvnply2  23791  pserdvlem2  23931  logeftb  24079  advlogexp  24146  cxpne0  24168  cxpp1  24171  lgsne0  24805  f1otrg  25497  ax5seglem9  25563  umgrass  25642  umgran0  25643  umgrale  25644  nbgraf1olem3  25766  pthdepisspth  25898  sspval  26756  sspnval  26770  lnof  26788  nmooval  26796  nmooge0  26800  nmoub3i  26806  bloln  26817  nmblore  26819  hosval  27777  homval  27778  hodval  27779  hfsval  27780  hfmval  27781  homulass  27839  hoadddir  27841  nmopub2tALT  27946  nmfnleub2  27963  kbval  27991  lnopmul  28004  0lnfn  28022  lnopcoi  28040  nmcoplb  28067  nmcfnlb  28091  kbass2  28154  nmopleid  28176  hstoh  28269  mdi  28332  dmdi  28339  dmdi4  28344  supxrnemnf  28718  reofld  28965  bnj605  30025  bnj607  30034  bnj1097  30097  elno2  30845  topdifinffinlem  32165  lindsdom  32367  lindsenlbs  32368  ftc1anclem2  32450  fzmul  32501  nninfnub  32511  exidreslem  32640  grposnOLD  32645  ghomf  32653  rngohomf  32729  rngohom1  32731  rngohomadd  32732  rngohommul  32733  rngoiso1o  32742  rngoisohom  32743  igenmin  32827  lkrcl  33191  lkrf0  33192  omlfh1N  33357  tendoex  35075  3anrabdioph  36158  3orrabdioph  36159  rencldnfilem  36196  expmordi  36324  dvdsabsmod0  36366  jm2.18  36367  jm2.25  36378  jm2.15nn0  36382  addrfv  37488  subrfv  37489  mulvfv  37490  bi3impa  37505  ssfiunibd  38258  dvnmul  38627  stoweidlem34  38721  stoweidlem48  38735  sge0cl  39068  sge0xp  39116  ovnsubaddlem1  39254  ovnovollem3  39342  aovmpt4g  39725  gboage9  39981  uhgrn0  40281  upgrn0  40307  upgrle  40308  uhgr1wlkspthlem2  40952
  Copyright terms: Public domain W3C validator