Theorem 3impa 1125

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-3an 1103

This theorem is referenced by:  3imp  1126  3adant1  1146  3adant2  1147  ex3  1363  3impdir  1368  syl3an9b  1460  biimp3a  1496  stoic3  1804  rspec3  3292  vtocl3gaf  3552  vtocl3ga  3553  rspc3v  3605  raltpg  4669  rextpg  4670  disjiun  5102  otthg  5471  3optocl  5762  fun2ssres  6585  funtpg  6595  funssfv  6906  f1elima  7265  ot1stg  8003  ot2ndg  8004  smogt  8357  omord2  8555  omword  8558  oeword  8579  omabslem  8639  ecovass  8825  fpmg  8869  findcard  9151  endjudisj  10155  cfsmolem  10257  ingru  10803  addasspi  10883  mulasspi  10885  ltapi  10891  ltmpi  10892  axpre-ltadd  11155  leltne  11302  dedekind  11376  recextlem2  11848  divdiv32  11926  divdiv1  11929  lble  12170  fnn0ind  12698  supminf  12962  xrleltne  13173  xrmaxeq  13208  xrmineq  13209  iccgelb  13432  elicc4  13443  iccsplit  13515  elfz  13544  modabs  13940  expgt0  14134  expge0  14137  expge1  14138  mulexpz  14141  expp1z  14150  expm1  14151  expmordi  14206  digit1  14276  faclbnd4  14336  faclbnd5  14337  ccatsymb  14623  s3eqs2s1eq  14978  abssubne0  15371  binom  15887  dvds0lem  16327  dvdsnegb  16334  muldvds1  16341  muldvds2  16342  dvdscmulr  16345  dvdsmulcr  16346  divalgmodcl  16468  gcd2n0cl  16570  gcdaddm  16586  lcmdvds  16669  prmdvdsexp  16777  rpexp1i  16785  monpropd  17797  prfval  18258  xpcpropd  18267  curf2ndf  18306  eqglact  19250  ghmqusker  19360  mndodcongi  19616  oddvdsnn0  19617  efgi0  19793  efgi1  19794  efgsval2  19806  lss0cl  21051  mpofrlmd  21910  evls1fpws  22512  scmatscmid  22646  pmatcollpw3fi1lem1  22926  cnpval  23376  cnf2  23389  cnnei  23422  lfinun  23665  ptpjcn  23751  cnmptk2  23826  flfval  24130  cnmpt2plusg  24228  cnmpt2vsca  24335  ustincl  24348  xbln0  24554  blssec  24575  blpnfctr  24576  mopni2  24633  mopni3  24634  nmoval  24855  nmocl  24860  isnghm2  24864  isnmhm2  24892  cnmpt2ds  24984  metdseq0  24995  cnmpt2ip  25390  caucfil  25425  mbfimasn  25774  dvnf  26069  dvnbss  26070  coemul  26392  dvply1  26428  dvnply2  26431  pserdvlem2  26571  logeftb  26728  advlogexp  26800  cxpne0  26822  cxpp1  26825  elno2  27798  f1otrg  29190  ax5seglem9  29257  uhgrn0  29387  upgrn0  29409  upgrle  29410  uhgrwkspthlem2  30073  frgrhash2wsp  30653  sspval  31045  sspnval  31059  lnof  31077  nmooval  31085  nmooge0  31089  nmoub3i  31095  bloln  31106  nmblore  31108  hosval  32062  homval  32063  hodval  32064  hfsval  32065  hfmval  32066  homulass  32124  hoadddir  32126  nmopub2tALT  32231  nmfnleub2  32248  kbval  32276  lnopmul  32289  0lnfn  32307  lnopcoi  32325  nmcoplb  32352  nmcfnlb  32376  kbass2  32439  nmopleid  32461  hstoh  32554  mdi  32617  dmdi  32624  dmdi4  32629  tpssg  32853  fdifsuppconst  33004  supxrnemnf  33083  elrgspnlem2  33533  rloccring  33561  reofld  33633  nsgmgclem  33690  rhmimaidl  33710  dfufd2lem  33809  r1plmhm  33869  r1pquslmic  33870  lbsdiflsp0  33986  evls1fldgencl  34030  zarclsun  34230  zarclsint  34232  bnj605  35265  bnj607  35274  bnj1097  35339  fnrelpredd  35450  rankfilimb  35464  cusgredgex  35572  topdifinffinlem  37941  lindsdom  38213  lindsenlbs  38214  ftc1anclem2  38293  fzmul  38340  nninfnub  38350  exidreslem  38476  grposnOLD  38481  ghomf  38489  rngohomf  38565  rngohom1  38567  rngohomadd  38568  rngohommul  38569  rngoiso1o  38578  rngoisohom  38579  igenmin  38663  lkrcl  39816  lkrf0  39817  omlfh1N  39982  tendoex  41699  uzindd  42695  primrootsunit1  42814  sticksstones3  42865  sticksstones10  42872  sticksstones12a  42874  sticksstones12  42875  sticksstones17  42880  3anrabdioph  43465  3orrabdioph  43466  rencldnfilem  43499  dvdsabsmod0  43666  jm2.18  43667  jm2.25  43678  jm2.15nn0  43682  tfsconcatlem  44015  onsucunitp  44052  addrfv  45129  subrfv  45130  mulvfv  45131  bi3impa  45146  ssfiunibd  45980  supminfxr  46130  limsupgtlem  46443  xlimmnfv  46500  xlimpnfv  46504  dvnmul  46609  stoweidlem34  46700  stoweidlem48  46714  sge0cl  47047  sge0xp  47095  ovnsubaddlem1  47236  aovmpt4g  47887  gboge9  48478