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  3257  vtocl3gaf  3547  vtocl3ga  3549  rspc3v  3604  raltpg  4662  rextpg  4663  disjiun  5095  otthg  5445  3optocl  5735  fun2ssres  6561  funtpg  6571  funssfv  6879  f1elima  7238  ot1stg  7982  ot2ndg  7983  smogt  8336  omord2  8531  omword  8534  oeword  8554  omabslem  8614  ecovass  8797  fpmg  8841  findcard  9127  endjudisj  10122  cfsmolem  10223  ingru  10768  addasspi  10848  mulasspi  10850  ltapi  10856  ltmpi  10857  axpre-ltadd  11120  leltne  11263  dedekind  11337  recextlem2  11809  divdiv32  11890  divdiv1  11893  lble  12135  fnn0ind  12633  supminf  12894  xrleltne  13105  xrmaxeq  13139  xrmineq  13140  iccgelb  13363  elicc4  13374  iccsplit  13446  elfz  13474  modabs  13866  expgt0  14060  expge0  14063  expge1  14064  mulexpz  14067  expp1z  14076  expm1  14077  expmordi  14132  digit1  14202  faclbnd4  14262  faclbnd5  14263  ccatsymb  14547  s3eqs2s1eq  14904  abssubne0  15283  binom  15796  dvds0lem  16236  dvdsnegb  16243  muldvds1  16250  muldvds2  16251  dvdscmulr  16254  dvdsmulcr  16255  divalgmodcl  16377  gcd2n0cl  16479  gcdaddm  16495  lcmdvds  16578  prmdvdsexp  16685  rpexp1i  16693  monpropd  17699  prfval  18160  xpcpropd  18169  curf2ndf  18208  eqglact  19111  ghmqusker  19219  mndodcongi  19473  oddvdsnn0  19474  efgi0  19650  efgi1  19651  efgsval2  19663  lss0cl  20853  mpofrlmd  21686  evls1fpws  22256  scmatscmid  22393  pmatcollpw3fi1lem1  22673  cnpval  23123  cnf2  23136  cnnei  23169  lfinun  23412  ptpjcn  23498  cnmptk2  23573  flfval  23877  cnmpt2plusg  23975  cnmpt2vsca  24082  ustincl  24095  xbln0  24302  blssec  24323  blpnfctr  24324  mopni2  24381  mopni3  24382  nmoval  24603  nmocl  24608  isnghm2  24612  isnmhm2  24640  cnmpt2ds  24732  metdseq0  24743  cnmpt2ip  25148  caucfil  25183  mbfimasn  25533  dvnf  25829  dvnbss  25830  coemul  26157  dvply1  26191  dvnply2  26195  pserdvlem2  26338  logeftb  26492  advlogexp  26564  cxpne0  26586  cxpp1  26589  elno2  27566  f1otrg  28798  ax5seglem9  28864  uhgrn0  28994  upgrn0  29016  upgrle  29017  uhgrwkspthlem2  29684  frgrhash2wsp  30261  sspval  30652  sspnval  30666  lnof  30684  nmooval  30692  nmooge0  30696  nmoub3i  30702  bloln  30713  nmblore  30715  hosval  31669  homval  31670  hodval  31671  hfsval  31672  hfmval  31673  homulass  31731  hoadddir  31733  nmopub2tALT  31838  nmfnleub2  31855  kbval  31883  lnopmul  31896  0lnfn  31914  lnopcoi  31932  nmcoplb  31959  nmcfnlb  31983  kbass2  32046  nmopleid  32068  hstoh  32161  mdi  32224  dmdi  32231  dmdi4  32236  tpssg  32466  fdifsuppconst  32612  supxrnemnf  32691  elrgspnlem2  33194  rloccring  33221  reofld  33315  nsgmgclem  33382  rhmimaidl  33403  dfufd2lem  33520  r1plmhm  33575  r1pquslmic  33576  lbsdiflsp0  33622  evls1fldgencl  33665  zarclsun  33860  zarclsint  33862  bnj605  34897  bnj607  34906  bnj1097  34971  fnrelpredd  35079  cusgredgex  35109  topdifinffinlem  37335  lindsdom  37608  lindsenlbs  37609  ftc1anclem2  37688  fzmul  37735  nninfnub  37745  exidreslem  37871  grposnOLD  37876  ghomf  37884  rngohomf  37960  rngohom1  37962  rngohomadd  37963  rngohommul  37964  rngoiso1o  37973  rngoisohom  37974  igenmin  38058  lkrcl  39085  lkrf0  39086  omlfh1N  39251  tendoex  40969  uzindd  41965  primrootsunit1  42085  sticksstones3  42136  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones17  42151  3anrabdioph  42770  3orrabdioph  42771  rencldnfilem  42808  dvdsabsmod0  42976  jm2.18  42977  jm2.25  42988  jm2.15nn0  42992  tfsconcatlem  43325  onsucunitp  43362  addrfv  44458  subrfv  44459  mulvfv  44460  bi3impa  44475  ssfiunibd  45307  supminfxr  45460  limsupgtlem  45775  xlimmnfv  45832  xlimpnfv  45836  dvnmul  45941  stoweidlem34  46032  stoweidlem48  46046  sge0cl  46379  sge0xp  46427  ovnsubaddlem1  46568  aovmpt4g  47202  gboge9  47765