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  1348  3impdir  1353  syl3an9b  1437  biimp3a  1472  stoic3  1778  rspec3  3258  vtocl3gaf  3525  vtocl3ga  3527  rspc3v  3581  raltpg  4643  rextpg  4644  disjiun  5074  otthg  5434  3optocl  5722  fun2ssres  6538  funtpg  6548  funssfv  6856  f1elima  7212  ot1stg  7950  ot2ndg  7951  smogt  8301  omord2  8496  omword  8499  oeword  8520  omabslem  8580  ecovass  8765  fpmg  8810  findcard  9092  endjudisj  10085  cfsmolem  10186  ingru  10732  addasspi  10812  mulasspi  10814  ltapi  10820  ltmpi  10821  axpre-ltadd  11084  leltne  11229  dedekind  11303  recextlem2  11775  divdiv32  11857  divdiv1  11860  lble  12102  fnn0ind  12622  supminf  12879  xrleltne  13090  xrmaxeq  13125  xrmineq  13126  iccgelb  13349  elicc4  13360  iccsplit  13432  elfz  13461  modabs  13857  expgt0  14051  expge0  14054  expge1  14055  mulexpz  14058  expp1z  14067  expm1  14068  expmordi  14123  digit1  14193  faclbnd4  14253  faclbnd5  14254  ccatsymb  14539  s3eqs2s1eq  14894  abssubne0  15273  binom  15789  dvds0lem  16229  dvdsnegb  16236  muldvds1  16243  muldvds2  16244  dvdscmulr  16247  dvdsmulcr  16248  divalgmodcl  16370  gcd2n0cl  16472  gcdaddm  16488  lcmdvds  16571  prmdvdsexp  16679  rpexp1i  16687  monpropd  17698  prfval  18159  xpcpropd  18168  curf2ndf  18207  eqglact  19148  ghmqusker  19256  mndodcongi  19512  oddvdsnn0  19513  efgi0  19689  efgi1  19690  efgsval2  19702  lss0cl  20936  mpofrlmd  21770  evls1fpws  22347  scmatscmid  22484  pmatcollpw3fi1lem1  22764  cnpval  23214  cnf2  23227  cnnei  23260  lfinun  23503  ptpjcn  23589  cnmptk2  23664  flfval  23968  cnmpt2plusg  24066  cnmpt2vsca  24173  ustincl  24186  xbln0  24392  blssec  24413  blpnfctr  24414  mopni2  24471  mopni3  24472  nmoval  24693  nmocl  24698  isnghm2  24702  isnmhm2  24730  cnmpt2ds  24822  metdseq0  24833  cnmpt2ip  25228  caucfil  25263  mbfimasn  25612  dvnf  25907  dvnbss  25908  coemul  26230  dvply1  26263  dvnply2  26267  pserdvlem2  26409  logeftb  26563  advlogexp  26635  cxpne0  26657  cxpp1  26660  elno2  27635  f1otrg  28956  ax5seglem9  29023  uhgrn0  29153  upgrn0  29175  upgrle  29176  uhgrwkspthlem2  29840  frgrhash2wsp  30420  sspval  30812  sspnval  30826  lnof  30844  nmooval  30852  nmooge0  30856  nmoub3i  30862  bloln  30873  nmblore  30875  hosval  31829  homval  31830  hodval  31831  hfsval  31832  hfmval  31833  homulass  31891  hoadddir  31893  nmopub2tALT  31998  nmfnleub2  32015  kbval  32043  lnopmul  32056  0lnfn  32074  lnopcoi  32092  nmcoplb  32119  nmcfnlb  32143  kbass2  32206  nmopleid  32228  hstoh  32321  mdi  32384  dmdi  32391  dmdi4  32396  tpssg  32625  fdifsuppconst  32780  supxrnemnf  32859  elrgspnlem2  33322  rloccring  33349  reofld  33421  nsgmgclem  33489  rhmimaidl  33510  dfufd2lem  33627  r1plmhm  33688  r1pquslmic  33689  lbsdiflsp0  33789  evls1fldgencl  33833  zarclsun  34033  zarclsint  34035  bnj605  35068  bnj607  35077  bnj1097  35142  fnrelpredd  35253  rankfilimb  35264  cusgredgex  35323  topdifinffinlem  37680  lindsdom  37952  lindsenlbs  37953  ftc1anclem2  38032  fzmul  38079  nninfnub  38089  exidreslem  38215  grposnOLD  38220  ghomf  38228  rngohomf  38304  rngohom1  38306  rngohomadd  38307  rngohommul  38308  rngoiso1o  38317  rngoisohom  38318  igenmin  38402  lkrcl  39555  lkrf0  39556  omlfh1N  39721  tendoex  41438  uzindd  42434  primrootsunit1  42553  sticksstones3  42604  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  sticksstones17  42619  3anrabdioph  43231  3orrabdioph  43232  rencldnfilem  43269  dvdsabsmod0  43436  jm2.18  43437  jm2.25  43448  jm2.15nn0  43452  tfsconcatlem  43785  onsucunitp  43822  addrfv  44916  subrfv  44917  mulvfv  44918  bi3impa  44933  ssfiunibd  45763  supminfxr  45913  limsupgtlem  46226  xlimmnfv  46283  xlimpnfv  46287  dvnmul  46392  stoweidlem34  46483  stoweidlem48  46497  sge0cl  46830  sge0xp  46878  ovnsubaddlem1  47019  aovmpt4g  47664  gboge9  48255