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  1347  3impdir  1352  syl3an9b  1436  biimp3a  1471  stoic3  1776  rspec3  3280  vtocl3gaf  3581  vtocl3ga  3583  rspc3v  3638  raltpg  4698  rextpg  4699  disjiun  5131  otthg  5490  3optocl  5782  fun2ssres  6611  funtpg  6621  funssfv  6927  f1elima  7283  ot1stg  8028  ot2ndg  8029  smogt  8407  omord2  8605  omword  8608  oeword  8628  omabslem  8688  ecovass  8864  fpmg  8908  findcard  9203  endjudisj  10209  cfsmolem  10310  ingru  10855  addasspi  10935  mulasspi  10937  ltapi  10943  ltmpi  10944  axpre-ltadd  11207  leltne  11350  dedekind  11424  recextlem2  11894  divdiv32  11975  divdiv1  11978  lble  12220  fnn0ind  12717  supminf  12977  xrleltne  13187  xrmaxeq  13221  xrmineq  13222  iccgelb  13443  elicc4  13454  iccsplit  13525  elfz  13553  modabs  13944  expgt0  14136  expge0  14139  expge1  14140  mulexpz  14143  expp1z  14152  expm1  14153  expmordi  14207  digit1  14276  faclbnd4  14336  faclbnd5  14337  ccatsymb  14620  s3eqs2s1eq  14977  abssubne0  15355  binom  15866  dvds0lem  16304  dvdsnegb  16311  muldvds1  16318  muldvds2  16319  dvdscmulr  16322  dvdsmulcr  16323  divalgmodcl  16444  gcd2n0cl  16546  gcdaddm  16562  lcmdvds  16645  prmdvdsexp  16752  rpexp1i  16760  monpropd  17781  prfval  18244  xpcpropd  18253  curf2ndf  18292  eqglact  19197  ghmqusker  19305  mndodcongi  19561  oddvdsnn0  19562  efgi0  19738  efgi1  19739  efgsval2  19751  lss0cl  20945  mpofrlmd  21797  evls1fpws  22373  scmatscmid  22512  pmatcollpw3fi1lem1  22792  cnpval  23244  cnf2  23257  cnnei  23290  lfinun  23533  ptpjcn  23619  cnmptk2  23694  flfval  23998  cnmpt2plusg  24096  cnmpt2vsca  24203  ustincl  24216  xbln0  24424  blssec  24445  blpnfctr  24446  mopni2  24506  mopni3  24507  nmoval  24736  nmocl  24741  isnghm2  24745  isnmhm2  24773  cnmpt2ds  24865  metdseq0  24876  cnmpt2ip  25282  caucfil  25317  mbfimasn  25667  dvnf  25963  dvnbss  25964  coemul  26291  dvply1  26325  dvnply2  26329  pserdvlem2  26472  logeftb  26625  advlogexp  26697  cxpne0  26719  cxpp1  26722  elno2  27699  f1otrg  28879  ax5seglem9  28952  uhgrn0  29084  upgrn0  29106  upgrle  29107  uhgrwkspthlem2  29774  frgrhash2wsp  30351  sspval  30742  sspnval  30756  lnof  30774  nmooval  30782  nmooge0  30786  nmoub3i  30792  bloln  30803  nmblore  30805  hosval  31759  homval  31760  hodval  31761  hfsval  31762  hfmval  31763  homulass  31821  hoadddir  31823  nmopub2tALT  31928  nmfnleub2  31945  kbval  31973  lnopmul  31986  0lnfn  32004  lnopcoi  32022  nmcoplb  32049  nmcfnlb  32073  kbass2  32136  nmopleid  32158  hstoh  32251  mdi  32314  dmdi  32321  dmdi4  32326  fdifsuppconst  32698  supxrnemnf  32772  elrgspnlem2  33247  rloccring  33274  reofld  33372  nsgmgclem  33439  rhmimaidl  33460  dfufd2lem  33577  r1plmhm  33630  r1pquslmic  33631  lbsdiflsp0  33677  evls1fldgencl  33720  zarclsun  33869  zarclsint  33871  bnj605  34921  bnj607  34930  bnj1097  34995  fnrelpredd  35103  cusgredgex  35127  topdifinffinlem  37348  lindsdom  37621  lindsenlbs  37622  ftc1anclem2  37701  fzmul  37748  nninfnub  37758  exidreslem  37884  grposnOLD  37889  ghomf  37897  rngohomf  37973  rngohom1  37975  rngohomadd  37976  rngohommul  37977  rngoiso1o  37986  rngoisohom  37987  igenmin  38071  lkrcl  39093  lkrf0  39094  omlfh1N  39259  tendoex  40977  uzindd  41978  primrootsunit1  42098  sticksstones3  42149  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones17  42164  3anrabdioph  42793  3orrabdioph  42794  rencldnfilem  42831  dvdsabsmod0  42999  jm2.18  43000  jm2.25  43011  jm2.15nn0  43015  tfsconcatlem  43349  onsucunitp  43386  addrfv  44488  subrfv  44489  mulvfv  44490  bi3impa  44505  ssfiunibd  45321  supminfxr  45475  limsupgtlem  45792  xlimmnfv  45849  xlimpnfv  45853  dvnmul  45958  stoweidlem34  46049  stoweidlem48  46063  sge0cl  46396  sge0xp  46444  ovnsubaddlem1  46585  aovmpt4g  47213  gboge9  47751