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  4573  otthg  4880  3optocl  5120  fun2ssres  5845  funtpg  5856  funssfv  6119  foco2OLD  6288  f1elima  6421  ot1stg  7073  ot2ndg  7074  smogt  7351  omord2  7534  omword  7537  oeword  7557  omabslem  7613  ecovass  7742  fpmg  7769  findcard  8084  cdaun  8877  cfsmolem  8975  ingru  9516  addasspi  9596  mulasspi  9598  ltapi  9604  ltmpi  9605  axpre-ltadd  9867  leltne  10006  dedekind  10079  recextlem2  10537  divdiv32  10612  divdiv1  10615  lble  10854  fnn0ind  11352  supminf  11651  xrleltne  11854  xrmaxeq  11884  xrmineq  11885  iccgelb  12101  elicc4  12111  iccsplit  12176  elfz  12203  fzrevral  12294  modabs  12565  expgt0  12755  expge0  12758  expge1  12759  mulexpz  12762  expp1z  12771  expm1  12772  digit1  12860  faclbnd4  12946  faclbnd5  12947  abssubne0  13904  binom  14401  dvds0lem  14830  dvdsnegb  14837  muldvds1  14844  muldvds2  14845  dvdscmulr  14848  dvdsmulcr  14849  divalgmodcl  14969  gcd2n0cl  15069  gcdaddm  15084  lcmdvds  15159  prmdvdsexp  15265  rpexp1i  15271  monpropd  16220  prfval  16662  xpcpropd  16671  curf2ndf  16710  eqglact  17468  mndodcongi  17785  oddvdsnn0  17786  efgi0  17956  efgi1  17957  lss0cl  18768  scmatscmid  20131  pmatcollpw3fi1lem1  20410  cnpval  20850  cnf2  20863  cnnei  20896  lfinun  21138  ptpjcn  21224  cnmptk2  21299  flfval  21604  cnmpt2plusg  21702  cnmpt2vsca  21808  ustincl  21821  xbln0  22029  blssec  22050  blpnfctr  22051  mopni2  22108  mopni3  22109  nmoval  22329  nmocl  22334  isnghm2  22338  isnmhm2  22366  cnmpt2ds  22454  metdseq0  22465  cnmpt2ip  22855  caucfil  22889  mbfimasn  23207  dvnf  23496  dvnbss  23497  coemul  23812  dvply1  23843  dvnply2  23846  pserdvlem2  23986  logeftb  24134  advlogexp  24201  cxpne0  24223  cxpp1  24226  lgsne0  24860  f1otrg  25551  ax5seglem9  25617  uhgrn0  25733  upgrn0  25756  upgrle  25757  umgrass  25848  umgran0  25849  umgrale  25850  nbgraf1olem3  25972  pthdepisspth  26104  sspval  26962  sspnval  26976  lnof  26994  nmooval  27002  nmooge0  27006  nmoub3i  27012  bloln  27023  nmblore  27025  hosval  27983  homval  27984  hodval  27985  hfsval  27986  hfmval  27987  homulass  28045  hoadddir  28047  nmopub2tALT  28152  nmfnleub2  28169  kbval  28197  lnopmul  28210  0lnfn  28228  lnopcoi  28246  nmcoplb  28273  nmcfnlb  28297  kbass2  28360  nmopleid  28382  hstoh  28475  mdi  28538  dmdi  28545  dmdi4  28550  supxrnemnf  28924  reofld  29171  bnj605  30231  bnj607  30240  bnj1097  30303  elno2  31051  topdifinffinlem  32371  lindsdom  32573  lindsenlbs  32574  ftc1anclem2  32656  fzmul  32707  nninfnub  32717  exidreslem  32846  grposnOLD  32851  ghomf  32859  rngohomf  32935  rngohom1  32937  rngohomadd  32938  rngohommul  32939  rngoiso1o  32948  rngoisohom  32949  igenmin  33033  lkrcl  33397  lkrf0  33398  omlfh1N  33563  tendoex  35281  3anrabdioph  36364  3orrabdioph  36365  rencldnfilem  36402  expmordi  36530  dvdsabsmod0  36572  jm2.18  36573  jm2.25  36584  jm2.15nn0  36588  addrfv  37694  subrfv  37695  mulvfv  37696  bi3impa  37711  ssfiunibd  38464  dvnmul  38833  stoweidlem34  38927  stoweidlem48  38941  sge0cl  39274  sge0xp  39322  ovnsubaddlem1  39460  ovnovollem3  39548  aovmpt4g  39930  gboage9  40186  uhgr1wlkspthlem2  40960
  Copyright terms: Public domain W3C validator