Theorem 3impa 1109

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

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

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 1088

This theorem is referenced by:  3imp  1110  3adant1  1130  3adant2  1131  ex3  1347  3impdir  1352  syl3an9b  1436  biimp3a  1471  stoic3  1776  rspec3  3255  vtocl3gaf  3544  vtocl3ga  3546  rspc3v  3601  raltpg  4658  rextpg  4659  disjiun  5090  otthg  5440  3optocl  5727  fun2ssres  6545  funtpg  6555  funssfv  6861  f1elima  7220  ot1stg  7961  ot2ndg  7962  smogt  8313  omord2  8508  omword  8511  oeword  8531  omabslem  8591  ecovass  8774  fpmg  8818  findcard  9104  endjudisj  10098  cfsmolem  10199  ingru  10744  addasspi  10824  mulasspi  10826  ltapi  10832  ltmpi  10833  axpre-ltadd  11096  leltne  11239  dedekind  11313  recextlem2  11785  divdiv32  11866  divdiv1  11869  lble  12111  fnn0ind  12609  supminf  12870  xrleltne  13081  xrmaxeq  13115  xrmineq  13116  iccgelb  13339  elicc4  13350  iccsplit  13422  elfz  13450  modabs  13842  expgt0  14036  expge0  14039  expge1  14040  mulexpz  14043  expp1z  14052  expm1  14053  expmordi  14108  digit1  14178  faclbnd4  14238  faclbnd5  14239  ccatsymb  14523  s3eqs2s1eq  14880  abssubne0  15259  binom  15772  dvds0lem  16212  dvdsnegb  16219  muldvds1  16226  muldvds2  16227  dvdscmulr  16230  dvdsmulcr  16231  divalgmodcl  16353  gcd2n0cl  16455  gcdaddm  16471  lcmdvds  16554  prmdvdsexp  16661  rpexp1i  16669  monpropd  17679  prfval  18140  xpcpropd  18149  curf2ndf  18188  eqglact  19093  ghmqusker  19201  mndodcongi  19457  oddvdsnn0  19458  efgi0  19634  efgi1  19635  efgsval2  19647  lss0cl  20885  mpofrlmd  21719  evls1fpws  22289  scmatscmid  22426  pmatcollpw3fi1lem1  22706  cnpval  23156  cnf2  23169  cnnei  23202  lfinun  23445  ptpjcn  23531  cnmptk2  23606  flfval  23910  cnmpt2plusg  24008  cnmpt2vsca  24115  ustincl  24128  xbln0  24335  blssec  24356  blpnfctr  24357  mopni2  24414  mopni3  24415  nmoval  24636  nmocl  24641  isnghm2  24645  isnmhm2  24673  cnmpt2ds  24765  metdseq0  24776  cnmpt2ip  25181  caucfil  25216  mbfimasn  25566  dvnf  25862  dvnbss  25863  coemul  26190  dvply1  26224  dvnply2  26228  pserdvlem2  26371  logeftb  26525  advlogexp  26597  cxpne0  26619  cxpp1  26622  elno2  27599  f1otrg  28851  ax5seglem9  28917  uhgrn0  29047  upgrn0  29069  upgrle  29070  uhgrwkspthlem2  29734  frgrhash2wsp  30311  sspval  30702  sspnval  30716  lnof  30734  nmooval  30742  nmooge0  30746  nmoub3i  30752  bloln  30763  nmblore  30765  hosval  31719  homval  31720  hodval  31721  hfsval  31722  hfmval  31723  homulass  31781  hoadddir  31783  nmopub2tALT  31888  nmfnleub2  31905  kbval  31933  lnopmul  31946  0lnfn  31964  lnopcoi  31982  nmcoplb  32009  nmcfnlb  32033  kbass2  32096  nmopleid  32118  hstoh  32211  mdi  32274  dmdi  32281  dmdi4  32286  tpssg  32516  fdifsuppconst  32662  supxrnemnf  32741  elrgspnlem2  33210  rloccring  33237  reofld  33308  nsgmgclem  33375  rhmimaidl  33396  dfufd2lem  33513  r1plmhm  33568  r1pquslmic  33569  lbsdiflsp0  33615  evls1fldgencl  33658  zarclsun  33853  zarclsint  33855  bnj605  34890  bnj607  34899  bnj1097  34964  fnrelpredd  35072  cusgredgex  35102  topdifinffinlem  37328  lindsdom  37601  lindsenlbs  37602  ftc1anclem2  37681  fzmul  37728  nninfnub  37738  exidreslem  37864  grposnOLD  37869  ghomf  37877  rngohomf  37953  rngohom1  37955  rngohomadd  37956  rngohommul  37957  rngoiso1o  37966  rngoisohom  37967  igenmin  38051  lkrcl  39078  lkrf0  39079  omlfh1N  39244  tendoex  40962  uzindd  41958  primrootsunit1  42078  sticksstones3  42129  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones17  42144  3anrabdioph  42763  3orrabdioph  42764  rencldnfilem  42801  dvdsabsmod0  42969  jm2.18  42970  jm2.25  42981  jm2.15nn0  42985  tfsconcatlem  43318  onsucunitp  43355  addrfv  44451  subrfv  44452  mulvfv  44453  bi3impa  44468  ssfiunibd  45300  supminfxr  45453  limsupgtlem  45768  xlimmnfv  45825  xlimpnfv  45829  dvnmul  45934  stoweidlem34  46025  stoweidlem48  46039  sge0cl  46372  sge0xp  46420  ovnsubaddlem1  46561  aovmpt4g  47195  gboge9  47758