Theorem 3impa 1110

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1111 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 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3impa.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 217	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-3an 1089

This theorem is referenced by:  3imp  1111  3adant1  1131  3adant2  1132  ex3  1348  3impdir  1353  syl3an9b  1437  biimp3a  1472  stoic3  1778  rspec3  3257  vtocl3gaf  3524  vtocl3ga  3526  rspc3v  3580  raltpg  4642  rextpg  4643  disjiun  5073  otthg  5438  3optocl  5728  fun2ssres  6543  funtpg  6553  funssfv  6861  f1elima  7218  ot1stg  7956  ot2ndg  7957  smogt  8307  omord2  8502  omword  8505  oeword  8526  omabslem  8586  ecovass  8771  fpmg  8816  findcard  9098  endjudisj  10091  cfsmolem  10192  ingru  10738  addasspi  10818  mulasspi  10820  ltapi  10826  ltmpi  10827  axpre-ltadd  11090  leltne  11235  dedekind  11309  recextlem2  11781  divdiv32  11863  divdiv1  11866  lble  12108  fnn0ind  12628  supminf  12885  xrleltne  13096  xrmaxeq  13131  xrmineq  13132  iccgelb  13355  elicc4  13366  iccsplit  13438  elfz  13467  modabs  13863  expgt0  14057  expge0  14060  expge1  14061  mulexpz  14064  expp1z  14073  expm1  14074  expmordi  14129  digit1  14199  faclbnd4  14259  faclbnd5  14260  ccatsymb  14545  s3eqs2s1eq  14900  abssubne0  15279  binom  15795  dvds0lem  16235  dvdsnegb  16242  muldvds1  16249  muldvds2  16250  dvdscmulr  16253  dvdsmulcr  16254  divalgmodcl  16376  gcd2n0cl  16478  gcdaddm  16494  lcmdvds  16577  prmdvdsexp  16685  rpexp1i  16693  monpropd  17704  prfval  18165  xpcpropd  18174  curf2ndf  18213  eqglact  19154  ghmqusker  19262  mndodcongi  19518  oddvdsnn0  19519  efgi0  19695  efgi1  19696  efgsval2  19708  lss0cl  20942  mpofrlmd  21757  evls1fpws  22334  scmatscmid  22471  pmatcollpw3fi1lem1  22751  cnpval  23201  cnf2  23214  cnnei  23247  lfinun  23490  ptpjcn  23576  cnmptk2  23651  flfval  23955  cnmpt2plusg  24053  cnmpt2vsca  24160  ustincl  24173  xbln0  24379  blssec  24400  blpnfctr  24401  mopni2  24458  mopni3  24459  nmoval  24680  nmocl  24685  isnghm2  24689  isnmhm2  24717  cnmpt2ds  24809  metdseq0  24820  cnmpt2ip  25215  caucfil  25250  mbfimasn  25599  dvnf  25894  dvnbss  25895  coemul  26217  dvply1  26250  dvnply2  26253  pserdvlem2  26393  logeftb  26547  advlogexp  26619  cxpne0  26641  cxpp1  26644  elno2  27618  f1otrg  28939  ax5seglem9  29006  uhgrn0  29136  upgrn0  29158  upgrle  29159  uhgrwkspthlem2  29822  frgrhash2wsp  30402  sspval  30794  sspnval  30808  lnof  30826  nmooval  30834  nmooge0  30838  nmoub3i  30844  bloln  30855  nmblore  30857  hosval  31811  homval  31812  hodval  31813  hfsval  31814  hfmval  31815  homulass  31873  hoadddir  31875  nmopub2tALT  31980  nmfnleub2  31997  kbval  32025  lnopmul  32038  0lnfn  32056  lnopcoi  32074  nmcoplb  32101  nmcfnlb  32125  kbass2  32188  nmopleid  32210  hstoh  32303  mdi  32366  dmdi  32373  dmdi4  32378  tpssg  32607  fdifsuppconst  32762  supxrnemnf  32841  elrgspnlem2  33304  rloccring  33331  reofld  33403  nsgmgclem  33471  rhmimaidl  33492  dfufd2lem  33609  r1plmhm  33670  r1pquslmic  33671  lbsdiflsp0  33770  evls1fldgencl  33814  zarclsun  34014  zarclsint  34016  bnj605  35049  bnj607  35058  bnj1097  35123  fnrelpredd  35234  rankfilimb  35245  cusgredgex  35304  topdifinffinlem  37663  lindsdom  37935  lindsenlbs  37936  ftc1anclem2  38015  fzmul  38062  nninfnub  38072  exidreslem  38198  grposnOLD  38203  ghomf  38211  rngohomf  38287  rngohom1  38289  rngohomadd  38290  rngohommul  38291  rngoiso1o  38300  rngoisohom  38301  igenmin  38385  lkrcl  39538  lkrf0  39539  omlfh1N  39704  tendoex  41421  uzindd  42417  primrootsunit1  42536  sticksstones3  42587  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones17  42602  3anrabdioph  43214  3orrabdioph  43215  rencldnfilem  43248  dvdsabsmod0  43415  jm2.18  43416  jm2.25  43427  jm2.15nn0  43431  tfsconcatlem  43764  onsucunitp  43801  addrfv  44895  subrfv  44896  mulvfv  44897  bi3impa  44912  ssfiunibd  45742  supminfxr  45892  limsupgtlem  46205  xlimmnfv  46262  xlimpnfv  46266  dvnmul  46371  stoweidlem34  46462  stoweidlem48  46476  sge0cl  46809  sge0xp  46857  ovnsubaddlem1  46998  aovmpt4g  47649  gboge9  48240