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

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

Proof of Theorem 3impa
StepHypRef Expression
1 df-3an 1081 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3impa.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 218 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-3an 1081
This theorem is referenced by:  3imp  1103  3adant1  1122  3adant2  1123  ex3  1338  3impdir  1343  syl3an9b  1425  biimp3a  1460  stoic3  1768  rspec3  3209  rspc3v  3633  raltpg  4626  rextpg  4627  disjiun  5044  otthg  5368  3optocl  5640  fun2ssres  6392  funtpg  6402  funssfv  6684  f1elima  7012  ot1stg  7692  ot2ndg  7693  smogt  7993  omord2  8182  omword  8185  oeword  8205  omabslem  8262  ecovass  8393  fpmg  8421  findcard  8745  endjudisj  9582  cfsmolem  9680  ingru  10225  addasspi  10305  mulasspi  10307  ltapi  10313  ltmpi  10314  axpre-ltadd  10577  leltne  10718  dedekind  10791  recextlem2  11259  divdiv32  11336  divdiv1  11339  lble  11581  fnn0ind  12069  supminf  12323  xrleltne  12526  xrmaxeq  12560  xrmineq  12561  iccgelb  12781  elicc4  12791  iccsplit  12859  elfz  12886  modabs  13260  expgt0  13450  expge0  13453  expge1  13454  mulexpz  13457  expp1z  13466  expm1  13467  expmordi  13519  digit1  13586  faclbnd4  13645  faclbnd5  13646  ccatsymb  13924  s3eqs2s1eq  14288  abssubne0  14664  binom  15173  dvds0lem  15608  dvdsnegb  15615  muldvds1  15622  muldvds2  15623  dvdscmulr  15626  dvdsmulcr  15627  divalgmodcl  15746  gcd2n0cl  15846  gcdaddm  15861  lcmdvds  15940  prmdvdsexp  16047  rpexp1i  16053  monpropd  16995  prfval  17437  xpcpropd  17446  curf2ndf  17485  eqglact  18269  mndodcongi  18600  oddvdsnn0  18601  efgi0  18775  efgi1  18776  efgsval2  18788  lss0cl  19647  mpofrlmd  20849  scmatscmid  21043  pmatcollpw3fi1lem1  21322  cnpval  21772  cnf2  21785  cnnei  21818  lfinun  22061  ptpjcn  22147  cnmptk2  22222  flfval  22526  cnmpt2plusg  22624  cnmpt2vsca  22730  ustincl  22743  xbln0  22951  blssec  22972  blpnfctr  22973  mopni2  23030  mopni3  23031  nmoval  23251  nmocl  23256  isnghm2  23260  isnmhm2  23288  cnmpt2ds  23378  metdseq0  23389  cnmpt2ip  23778  caucfil  23813  mbfimasn  24160  dvnf  24451  dvnbss  24452  coemul  24769  dvply1  24800  dvnply2  24803  pserdvlem2  24943  logeftb  25094  advlogexp  25165  cxpne0  25187  cxpp1  25190  f1otrg  26584  ax5seglem9  26650  uhgrn0  26779  upgrn0  26801  upgrle  26802  uhgrwkspthlem2  27462  frgrhash2wsp  28038  sspval  28427  sspnval  28441  lnof  28459  nmooval  28467  nmooge0  28471  nmoub3i  28477  bloln  28488  nmblore  28490  hosval  29444  homval  29445  hodval  29446  hfsval  29447  hfmval  29448  homulass  29506  hoadddir  29508  nmopub2tALT  29613  nmfnleub2  29630  kbval  29658  lnopmul  29671  0lnfn  29689  lnopcoi  29707  nmcoplb  29734  nmcfnlb  29758  kbass2  29821  nmopleid  29843  hstoh  29936  mdi  29999  dmdi  30006  dmdi4  30011  supxrnemnf  30419  reofld  30840  lbsdiflsp0  30921  bnj605  32078  bnj607  32087  bnj1097  32150  cusgredgex  32265  elno2  33058  topdifinffinlem  34510  lindsdom  34767  lindsenlbs  34768  ftc1anclem2  34849  fzmul  34897  nninfnub  34907  exidreslem  35036  grposnOLD  35041  ghomf  35049  rngohomf  35125  rngohom1  35127  rngohomadd  35128  rngohommul  35129  rngoiso1o  35138  rngoisohom  35139  igenmin  35223  lkrcl  36108  lkrf0  36109  omlfh1N  36274  tendoex  37991  3anrabdioph  39257  3orrabdioph  39258  rencldnfilem  39295  dvdsabsmod0  39462  jm2.18  39463  jm2.25  39474  jm2.15nn0  39478  addrfv  40678  subrfv  40679  mulvfv  40680  bi3impa  40695  ssfiunibd  41452  supminfxr  41616  limsupgtlem  41934  xlimmnfv  41991  xlimpnfv  41995  dvnmul  42104  stoweidlem34  42196  stoweidlem48  42210  sge0cl  42540  sge0xp  42588  ovnsubaddlem1  42729  aovmpt4g  43277  gboge9  43806
  Copyright terms: Public domain W3C validator