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

Theorem 3impa 1111
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1112 by Wolf Lammen, 20-Jun-2022.)
Hypothesis
Ref Expression
3impa.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
3impa ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impa
StepHypRef Expression
1 df-3an 1090 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3impa.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 216 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-3an 1090
This theorem is referenced by:  3imp  1112  3adant1  1131  3adant2  1132  ex3  1347  3impdir  1352  syl3an9b  1435  biimp3a  1470  stoic3  1779  rspec3  3264  rspc3v  3594  raltpg  4660  rextpg  4661  disjiun  5093  otthg  5443  3optocl  5729  fun2ssres  6547  funtpg  6557  funssfv  6864  f1elima  7211  ot1stg  7936  ot2ndg  7937  smogt  8314  omord2  8515  omword  8518  oeword  8538  omabslem  8597  ecovass  8764  fpmg  8807  findcard  9108  endjudisj  10105  cfsmolem  10207  ingru  10752  addasspi  10832  mulasspi  10834  ltapi  10840  ltmpi  10841  axpre-ltadd  11104  leltne  11245  dedekind  11319  recextlem2  11787  divdiv32  11864  divdiv1  11867  lble  12108  fnn0ind  12603  supminf  12861  xrleltne  13065  xrmaxeq  13099  xrmineq  13100  iccgelb  13321  elicc4  13332  iccsplit  13403  elfz  13431  modabs  13810  expgt0  14002  expge0  14005  expge1  14006  mulexpz  14009  expp1z  14018  expm1  14019  expmordi  14073  digit1  14141  faclbnd4  14198  faclbnd5  14199  ccatsymb  14471  s3eqs2s1eq  14828  abssubne0  15202  binom  15716  dvds0lem  16150  dvdsnegb  16157  muldvds1  16164  muldvds2  16165  dvdscmulr  16168  dvdsmulcr  16169  divalgmodcl  16290  gcd2n0cl  16390  gcdaddm  16406  lcmdvds  16485  prmdvdsexp  16592  rpexp1i  16600  monpropd  17621  prfval  18088  xpcpropd  18098  curf2ndf  18137  eqglact  18982  mndodcongi  19326  oddvdsnn0  19327  efgi0  19503  efgi1  19504  efgsval2  19516  lss0cl  20410  mpofrlmd  21186  scmatscmid  21858  pmatcollpw3fi1lem1  22138  cnpval  22590  cnf2  22603  cnnei  22636  lfinun  22879  ptpjcn  22965  cnmptk2  23040  flfval  23344  cnmpt2plusg  23442  cnmpt2vsca  23549  ustincl  23562  xbln0  23770  blssec  23791  blpnfctr  23792  mopni2  23852  mopni3  23853  nmoval  24082  nmocl  24087  isnghm2  24091  isnmhm2  24119  cnmpt2ds  24209  metdseq0  24220  cnmpt2ip  24615  caucfil  24650  mbfimasn  24999  dvnf  25294  dvnbss  25295  coemul  25616  dvply1  25647  dvnply2  25650  pserdvlem2  25790  logeftb  25942  advlogexp  26013  cxpne0  26035  cxpp1  26038  elno2  27005  f1otrg  27816  ax5seglem9  27889  uhgrn0  28021  upgrn0  28043  upgrle  28044  uhgrwkspthlem2  28705  frgrhash2wsp  29279  sspval  29668  sspnval  29682  lnof  29700  nmooval  29708  nmooge0  29712  nmoub3i  29718  bloln  29729  nmblore  29731  hosval  30685  homval  30686  hodval  30687  hfsval  30688  hfmval  30689  homulass  30747  hoadddir  30749  nmopub2tALT  30854  nmfnleub2  30871  kbval  30899  lnopmul  30912  0lnfn  30930  lnopcoi  30948  nmcoplb  30975  nmcfnlb  30999  kbass2  31062  nmopleid  31084  hstoh  31177  mdi  31240  dmdi  31247  dmdi4  31252  fdifsuppconst  31607  supxrnemnf  31676  reofld  32139  nsgmgclem  32192  ghmqusker  32201  rhmimaidl  32209  evls1fpws  32274  lbsdiflsp0  32324  zarclsun  32454  zarclsint  32456  bnj605  33522  bnj607  33531  bnj1097  33596  fnrelpredd  33696  cusgredgex  33718  topdifinffinlem  35821  lindsdom  36075  lindsenlbs  36076  ftc1anclem2  36155  fzmul  36203  nninfnub  36213  exidreslem  36339  grposnOLD  36344  ghomf  36352  rngohomf  36428  rngohom1  36430  rngohomadd  36431  rngohommul  36432  rngoiso1o  36441  rngoisohom  36442  igenmin  36526  lkrcl  37557  lkrf0  37558  omlfh1N  37723  tendoex  39441  uzindd  40437  sticksstones3  40559  sticksstones10  40566  sticksstones12a  40568  sticksstones12  40569  sticksstones17  40574  3anrabdioph  41108  3orrabdioph  41109  rencldnfilem  41146  dvdsabsmod0  41314  jm2.18  41315  jm2.25  41326  jm2.15nn0  41330  addrfv  42756  subrfv  42757  mulvfv  42758  bi3impa  42773  ssfiunibd  43550  supminfxr  43706  limsupgtlem  44025  xlimmnfv  44082  xlimpnfv  44086  dvnmul  44191  stoweidlem34  44282  stoweidlem48  44296  sge0cl  44629  sge0xp  44677  ovnsubaddlem1  44818  aovmpt4g  45440  gboge9  45963
  Copyright terms: Public domain W3C validator