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  3249  vtocl3gaf  3536  vtocl3ga  3538  rspc3v  3593  raltpg  4650  rextpg  4651  disjiun  5080  otthg  5428  3optocl  5716  fun2ssres  6527  funtpg  6537  funssfv  6843  f1elima  7200  ot1stg  7938  ot2ndg  7939  smogt  8290  omord2  8485  omword  8488  oeword  8508  omabslem  8568  ecovass  8751  fpmg  8795  findcard  9077  endjudisj  10063  cfsmolem  10164  ingru  10709  addasspi  10789  mulasspi  10791  ltapi  10797  ltmpi  10798  axpre-ltadd  11061  leltne  11205  dedekind  11279  recextlem2  11751  divdiv32  11832  divdiv1  11835  lble  12077  fnn0ind  12575  supminf  12836  xrleltne  13047  xrmaxeq  13081  xrmineq  13082  iccgelb  13305  elicc4  13316  iccsplit  13388  elfz  13416  modabs  13808  expgt0  14002  expge0  14005  expge1  14006  mulexpz  14009  expp1z  14018  expm1  14019  expmordi  14074  digit1  14144  faclbnd4  14204  faclbnd5  14205  ccatsymb  14489  s3eqs2s1eq  14845  abssubne0  15224  binom  15737  dvds0lem  16177  dvdsnegb  16184  muldvds1  16191  muldvds2  16192  dvdscmulr  16195  dvdsmulcr  16196  divalgmodcl  16318  gcd2n0cl  16420  gcdaddm  16436  lcmdvds  16519  prmdvdsexp  16626  rpexp1i  16634  monpropd  17644  prfval  18105  xpcpropd  18114  curf2ndf  18153  eqglact  19058  ghmqusker  19166  mndodcongi  19422  oddvdsnn0  19423  efgi0  19599  efgi1  19600  efgsval2  19612  lss0cl  20850  mpofrlmd  21684  evls1fpws  22254  scmatscmid  22391  pmatcollpw3fi1lem1  22671  cnpval  23121  cnf2  23134  cnnei  23167  lfinun  23410  ptpjcn  23496  cnmptk2  23571  flfval  23875  cnmpt2plusg  23973  cnmpt2vsca  24080  ustincl  24093  xbln0  24300  blssec  24321  blpnfctr  24322  mopni2  24379  mopni3  24380  nmoval  24601  nmocl  24606  isnghm2  24610  isnmhm2  24638  cnmpt2ds  24730  metdseq0  24741  cnmpt2ip  25146  caucfil  25181  mbfimasn  25531  dvnf  25827  dvnbss  25828  coemul  26155  dvply1  26189  dvnply2  26193  pserdvlem2  26336  logeftb  26490  advlogexp  26562  cxpne0  26584  cxpp1  26587  elno2  27564  f1otrg  28816  ax5seglem9  28882  uhgrn0  29012  upgrn0  29034  upgrle  29035  uhgrwkspthlem2  29699  frgrhash2wsp  30276  sspval  30667  sspnval  30681  lnof  30699  nmooval  30707  nmooge0  30711  nmoub3i  30717  bloln  30728  nmblore  30730  hosval  31684  homval  31685  hodval  31686  hfsval  31687  hfmval  31688  homulass  31746  hoadddir  31748  nmopub2tALT  31853  nmfnleub2  31870  kbval  31898  lnopmul  31911  0lnfn  31929  lnopcoi  31947  nmcoplb  31974  nmcfnlb  31998  kbass2  32061  nmopleid  32083  hstoh  32176  mdi  32239  dmdi  32246  dmdi4  32251  tpssg  32481  fdifsuppconst  32632  supxrnemnf  32712  elrgspnlem2  33184  rloccring  33211  reofld  33282  nsgmgclem  33349  rhmimaidl  33370  dfufd2lem  33487  r1plmhm  33543  r1pquslmic  33544  lbsdiflsp0  33599  evls1fldgencl  33643  zarclsun  33843  zarclsint  33845  bnj605  34880  bnj607  34889  bnj1097  34954  fnrelpredd  35062  cusgredgex  35105  topdifinffinlem  37331  lindsdom  37604  lindsenlbs  37605  ftc1anclem2  37684  fzmul  37731  nninfnub  37741  exidreslem  37867  grposnOLD  37872  ghomf  37880  rngohomf  37956  rngohom1  37958  rngohomadd  37959  rngohommul  37960  rngoiso1o  37969  rngoisohom  37970  igenmin  38054  lkrcl  39081  lkrf0  39082  omlfh1N  39247  tendoex  40964  uzindd  41960  primrootsunit1  42080  sticksstones3  42131  sticksstones10  42138  sticksstones12a  42140  sticksstones12  42141  sticksstones17  42146  3anrabdioph  42765  3orrabdioph  42766  rencldnfilem  42803  dvdsabsmod0  42970  jm2.18  42971  jm2.25  42982  jm2.15nn0  42986  tfsconcatlem  43319  onsucunitp  43356  addrfv  44452  subrfv  44453  mulvfv  44454  bi3impa  44469  ssfiunibd  45301  supminfxr  45453  limsupgtlem  45768  xlimmnfv  45825  xlimpnfv  45829  dvnmul  45934  stoweidlem34  46025  stoweidlem48  46039  sge0cl  46372  sge0xp  46420  ovnsubaddlem1  46561  aovmpt4g  47195  gboge9  47758