Theorem 3impa 1091

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1069

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 199  df-3an 1071

This theorem is referenced by:  3imp  1092  3adant1  1111  3adant2  1112  ex3  1327  3impdir  1332  syl3an9b  1414  biimp3a  1449  stoic3  1740  rspec3  3164  rspc3v  3553  raltpg  4513  rextpg  4514  disjiun  4922  otthg  5238  3optocl  5501  fun2ssres  6237  funtpg  6247  funssfv  6525  f1elima  6852  ot1stg  7521  ot2ndg  7522  smogt  7814  omord2  8000  omword  8003  oeword  8023  omabslem  8079  ecovass  8210  fpmg  8238  findcard  8558  endjudisj  9398  cfsmolem  9496  ingru  10041  addasspi  10121  mulasspi  10123  ltapi  10129  ltmpi  10130  axpre-ltadd  10393  leltne  10536  dedekind  10609  recextlem2  11078  divdiv32  11155  divdiv1  11158  lble  11400  fnn0ind  11900  supminf  12155  xrleltne  12361  xrmaxeq  12395  xrmineq  12396  iccgelb  12615  elicc4  12625  iccsplit  12693  elfz  12720  modabs  13093  expgt0  13283  expge0  13286  expge1  13287  mulexpz  13290  expp1z  13299  expm1  13300  expmordi  13352  digit1  13419  faclbnd4  13478  faclbnd5  13479  s3eqs2s1eq  14168  abssubne0  14543  binom  15051  dvds0lem  15486  dvdsnegb  15493  muldvds1  15500  muldvds2  15501  dvdscmulr  15504  dvdsmulcr  15505  divalgmodcl  15624  gcd2n0cl  15724  gcdaddm  15739  lcmdvds  15814  prmdvdsexp  15921  rpexp1i  15927  monpropd  16877  prfval  17319  xpcpropd  17328  curf2ndf  17367  eqglact  18126  mndodcongi  18445  oddvdsnn0  18446  efgi0  18616  efgi1  18617  lss0cl  19452  mpofrlmd  20638  scmatscmid  20834  pmatcollpw3fi1lem1  21113  cnpval  21563  cnf2  21576  cnnei  21609  lfinun  21852  ptpjcn  21938  cnmptk2  22013  flfval  22317  cnmpt2plusg  22415  cnmpt2vsca  22521  ustincl  22534  xbln0  22742  blssec  22763  blpnfctr  22764  mopni2  22821  mopni3  22822  nmoval  23042  nmocl  23047  isnghm2  23051  isnmhm2  23079  cnmpt2ds  23169  metdseq0  23180  cnmpt2ip  23569  caucfil  23604  mbfimasn  23951  dvnf  24242  dvnbss  24243  coemul  24560  dvply1  24591  dvnply2  24594  pserdvlem2  24734  logeftb  24883  advlogexp  24954  cxpne0  24976  cxpp1  24979  f1otrg  26375  ax5seglem9  26441  uhgrn0  26570  upgrn0  26592  upgrle  26593  uhgrwkspthlem2  27258  frgrhash2wsp  27881  sspval  28292  sspnval  28306  lnof  28324  nmooval  28332  nmooge0  28336  nmoub3i  28342  bloln  28353  nmblore  28355  hosval  29313  homval  29314  hodval  29315  hfsval  29316  hfmval  29317  homulass  29375  hoadddir  29377  nmopub2tALT  29482  nmfnleub2  29499  kbval  29527  lnopmul  29540  0lnfn  29558  lnopcoi  29576  nmcoplb  29603  nmcfnlb  29627  kbass2  29690  nmopleid  29712  hstoh  29805  mdi  29868  dmdi  29875  dmdi4  29880  supxrnemnf  30269  reofld  30624  lbsdiflsp0  30683  bnj605  31858  bnj607  31867  bnj1097  31930  elno2  32722  topdifinffinlem  34110  lindsdom  34367  lindsenlbs  34368  ftc1anclem2  34449  fzmul  34498  nninfnub  34508  exidreslem  34637  grposnOLD  34642  ghomf  34650  rngohomf  34726  rngohom1  34728  rngohomadd  34729  rngohommul  34730  rngoiso1o  34739  rngoisohom  34740  igenmin  34824  lkrcl  35713  lkrf0  35714  omlfh1N  35879  tendoex  37596  3anrabdioph  38816  3orrabdioph  38817  rencldnfilem  38854  dvdsabsmod0  39021  jm2.18  39022  jm2.25  39033  jm2.15nn0  39037  addrfv  40260  subrfv  40261  mulvfv  40262  bi3impa  40277  ssfiunibd  41040  supminfxr  41206  limsupgtlem  41524  xlimmnfv  41581  xlimpnfv  41585  dvnmul  41693  stoweidlem34  41785  stoweidlem48  41799  sge0cl  42129  sge0xp  42177  ovnsubaddlem1  42318  aovmpt4g  42841  gboge9  43332