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

Step	Hyp	Ref	Expression
1		df-3an 1090	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3impa.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 216	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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  3278  rspc3v  3628  raltpg  4703  rextpg  4704  disjiun  5136  otthg  5486  3optocl  5773  fun2ssres  6594  funtpg  6604  funssfv  6913  f1elima  7262  ot1stg  7989  ot2ndg  7990  smogt  8367  omord2  8567  omword  8570  oeword  8590  omabslem  8649  ecovass  8818  fpmg  8862  findcard  9163  endjudisj  10163  cfsmolem  10265  ingru  10810  addasspi  10890  mulasspi  10892  ltapi  10898  ltmpi  10899  axpre-ltadd  11162  leltne  11303  dedekind  11377  recextlem2  11845  divdiv32  11922  divdiv1  11925  lble  12166  fnn0ind  12661  supminf  12919  xrleltne  13124  xrmaxeq  13158  xrmineq  13159  iccgelb  13380  elicc4  13391  iccsplit  13462  elfz  13490  modabs  13869  expgt0  14061  expge0  14064  expge1  14065  mulexpz  14068  expp1z  14077  expm1  14078  expmordi  14132  digit1  14200  faclbnd4  14257  faclbnd5  14258  ccatsymb  14532  s3eqs2s1eq  14889  abssubne0  15263  binom  15776  dvds0lem  16210  dvdsnegb  16217  muldvds1  16224  muldvds2  16225  dvdscmulr  16228  dvdsmulcr  16229  divalgmodcl  16350  gcd2n0cl  16450  gcdaddm  16466  lcmdvds  16545  prmdvdsexp  16652  rpexp1i  16660  monpropd  17684  prfval  18151  xpcpropd  18161  curf2ndf  18200  eqglact  19059  mndodcongi  19411  oddvdsnn0  19412  efgi0  19588  efgi1  19589  efgsval2  19601  lss0cl  20557  mpofrlmd  21332  scmatscmid  22008  pmatcollpw3fi1lem1  22288  cnpval  22740  cnf2  22753  cnnei  22786  lfinun  23029  ptpjcn  23115  cnmptk2  23190  flfval  23494  cnmpt2plusg  23592  cnmpt2vsca  23699  ustincl  23712  xbln0  23920  blssec  23941  blpnfctr  23942  mopni2  24002  mopni3  24003  nmoval  24232  nmocl  24237  isnghm2  24241  isnmhm2  24269  cnmpt2ds  24359  metdseq0  24370  cnmpt2ip  24765  caucfil  24800  mbfimasn  25149  dvnf  25444  dvnbss  25445  coemul  25766  dvply1  25797  dvnply2  25800  pserdvlem2  25940  logeftb  26092  advlogexp  26163  cxpne0  26185  cxpp1  26188  elno2  27157  f1otrg  28122  ax5seglem9  28195  uhgrn0  28327  upgrn0  28349  upgrle  28350  uhgrwkspthlem2  29011  frgrhash2wsp  29585  sspval  29976  sspnval  29990  lnof  30008  nmooval  30016  nmooge0  30020  nmoub3i  30026  bloln  30037  nmblore  30039  hosval  30993  homval  30994  hodval  30995  hfsval  30996  hfmval  30997  homulass  31055  hoadddir  31057  nmopub2tALT  31162  nmfnleub2  31179  kbval  31207  lnopmul  31220  0lnfn  31238  lnopcoi  31256  nmcoplb  31283  nmcfnlb  31307  kbass2  31370  nmopleid  31392  hstoh  31485  mdi  31548  dmdi  31555  dmdi4  31560  fdifsuppconst  31911  supxrnemnf  31981  reofld  32459  nsgmgclem  32522  ghmqusker  32532  rhmimaidl  32550  evls1fpws  32646  lbsdiflsp0  32711  zarclsun  32850  zarclsint  32852  bnj605  33918  bnj607  33927  bnj1097  33992  fnrelpredd  34092  cusgredgex  34112  topdifinffinlem  36228  lindsdom  36482  lindsenlbs  36483  ftc1anclem2  36562  fzmul  36609  nninfnub  36619  exidreslem  36745  grposnOLD  36750  ghomf  36758  rngohomf  36834  rngohom1  36836  rngohomadd  36837  rngohommul  36838  rngoiso1o  36847  rngoisohom  36848  igenmin  36932  lkrcl  37962  lkrf0  37963  omlfh1N  38128  tendoex  39846  uzindd  40842  sticksstones3  40964  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  sticksstones17  40979  3anrabdioph  41520  3orrabdioph  41521  rencldnfilem  41558  dvdsabsmod0  41726  jm2.18  41727  jm2.25  41738  jm2.15nn0  41742  tfsconcatlem  42086  onsucunitp  42123  addrfv  43228  subrfv  43229  mulvfv  43230  bi3impa  43245  ssfiunibd  44019  supminfxr  44174  limsupgtlem  44493  xlimmnfv  44550  xlimpnfv  44554  dvnmul  44659  stoweidlem34  44750  stoweidlem48  44764  sge0cl  45097  sge0xp  45145  ovnsubaddlem1  45286  aovmpt4g  45909  gboge9  46432