Theorem 3impa 1127

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-3an 1105

This theorem is used by:  3imp  1128  3adant1  1148  3adant2  1149  ex3  1365  3impdir  1370  syl3an9b  1462  biimp3a  1498  stoic3  1809  rspec3  3282  vtocl3gaf  3539  vtocl3ga  3540  rspc3v  3592  raltpg  4659  rextpg  4660  disjiun  5091  otthg  5461  3optocl  5752  fun2ssres  6579  funtpg  6589  funssfv  6900  f1elima  7261  ot1stg  8001  ot2ndg  8002  smogt  8357  omord2  8557  omword  8560  oeword  8581  omabslem  8641  ecovass  8827  fpmg  8878  findcard  9161  endjudisj  10174  cfsmolem  10275  ingru  10827  addasspi  10907  mulasspi  10909  ltapi  10915  ltmpi  10916  axpre-ltadd  11179  leltne  11326  dedekind  11400  recextlem2  11872  divdiv32  11950  divdiv1  11953  lble  12194  fnn0ind  12723  supminf  12987  xrleltne  13199  xrmaxeq  13234  xrmineq  13235  iccgelb  13458  elicc4  13469  iccsplit  13541  elfz  13570  modabs  13968  expgt0  14162  expge0  14165  expge1  14166  mulexpz  14169  expp1z  14178  expm1  14179  expmordi  14234  digit1  14304  faclbnd4  14364  faclbnd5  14365  ccatsymb  14651  s3eqs2s1eq  15012  abssubne0  15407  binom  15922  dvds0lem  16359  dvdsnegb  16366  muldvds1  16373  muldvds2  16374  dvdscmulr  16377  dvdsmulcr  16378  divalgmodcl  16500  gcd2n0cl  16602  gcdaddm  16618  lcmdvds  16701  prmdvdsexp  16809  rpexp1i  16817  monpropd  17829  prfval  18290  xpcpropd  18299  curf2ndf  18338  eqglact  19307  ghmqusker  19417  mndodcongi  19673  oddvdsnn0  19674  efgi0  19850  efgi1  19851  efgsval2  19863  lss0cl  21134  mpofrlmd  21993  lindsdom  22066  lindsenlbs  22067  evls1fpws  22597  scmatscmid  22731  pmatcollpw3fi1lem1  23014  cnpval  23464  cnf2  23477  cnnei  23510  lfinun  23754  ptpjcn  23840  cnmptk2  23915  flfval  24219  cnmpt2plusg  24317  cnmpt2vsca  24424  ustincl  24437  xbln0  24643  blssec  24664  blpnfctr  24665  mopni2  24722  mopni3  24723  nmoval  24944  nmocl  24949  isnghm2  24953  isnmhm2  24981  cnmpt2ds  25073  metdseq0  25084  cnmpt2ip  25479  caucfil  25514  mbfimasn  25863  dvnf  26157  dvnbss  26158  coemul  26481  dvply1  26517  dvnply2  26520  pserdvlem2  26667  logeftb  26823  advlogexp  26895  cxpne0  26917  cxpp1  26920  elno2  27893  f1otrg  29330  ax5seglem9  29397  uhgrn0  29527  upgrn0  29549  upgrle  29550  uhgrwkspthlem2  30222  frgrhash2wsp  30815  sspval  31207  sspnval  31221  lnof  31239  nmooval  31247  nmooge0  31251  nmoub3i  31257  bloln  31268  nmblore  31270  hosval  32224  homval  32225  hodval  32226  hfsval  32227  hfmval  32228  homulass  32286  hoadddir  32288  nmopub2tALT  32393  nmfnleub2  32410  kbval  32438  lnopmul  32451  0lnfn  32469  lnopcoi  32487  nmcoplb  32514  nmcfnlb  32538  kbass2  32601  nmopleid  32623  hstoh  32716  mdi  32779  dmdi  32786  dmdi4  32791  tpssg  33015  fdifsuppconst  33164  supxrnemnf  33242  elrgspnlem2  33686  rloccring  33714  reofld  33786  nsgmgclem  33843  rhmimaidl  33863  dfufd2lem  33962  r1plmhm  34022  r1pquslmic  34023  lbsdiflsp0  34139  evls1fldgencl  34183  zarclsun  34383  zarclsint  34385  bnj605  35419  bnj607  35428  bnj1097  35493  fnrelpredd  35599  rankfilimb  35613  cusgredgex  35723  topdifinffinlem  38104  ftc1anclem2  38446  fzmul  38494  nninfnub  38504  exidreslem  38630  grposnOLD  38635  ghomf  38643  rngohomf  38719  rngohom1  38721  rngohomadd  38722  rngohommul  38723  rngoiso1o  38732  rngoisohom  38733  igenmin  38817  lkrcl  39968  lkrf0  39969  omlfh1N  40134  tendoex  41851  uzindd  42847  primrootsunit1  42966  sticksstones3  43017  sticksstones10  43024  sticksstones12a  43026  sticksstones12  43027  sticksstones17  43032  3anrabdioph  43630  3orrabdioph  43631  rencldnfilem  43664  dvdsabsmod0  43831  jm2.18  43832  jm2.25  43843  jm2.15nn0  43847  tfsconcatlem  44180  onsucunitp  44217  addrfv  45294  subrfv  45295  mulvfv  45296  bi3impa  45311  ssfiunibd  46145  supminfxr  46295  limsupgtlem  46608  xlimmnfv  46665  xlimpnfv  46669  dvnmul  46774  stoweidlem34  46865  stoweidlem48  46879  sge0cl  47212  sge0xp  47260  ovnsubaddlem1  47401  aovmpt4g  48092  gboge9  48683