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  1777  rspec3  3256  vtocl3gaf  3536  vtocl3ga  3538  rspc3v  3592  raltpg  4655  rextpg  4656  disjiun  5086  otthg  5433  3optocl  5721  fun2ssres  6537  funtpg  6547  funssfv  6855  f1elima  7209  ot1stg  7947  ot2ndg  7948  smogt  8299  omord2  8494  omword  8497  oeword  8518  omabslem  8578  ecovass  8761  fpmg  8806  findcard  9088  endjudisj  10079  cfsmolem  10180  ingru  10726  addasspi  10806  mulasspi  10808  ltapi  10814  ltmpi  10815  axpre-ltadd  11078  leltne  11222  dedekind  11296  recextlem2  11768  divdiv32  11849  divdiv1  11852  lble  12094  fnn0ind  12591  supminf  12848  xrleltne  13059  xrmaxeq  13094  xrmineq  13095  iccgelb  13318  elicc4  13329  iccsplit  13401  elfz  13429  modabs  13824  expgt0  14018  expge0  14021  expge1  14022  mulexpz  14025  expp1z  14034  expm1  14035  expmordi  14090  digit1  14160  faclbnd4  14220  faclbnd5  14221  ccatsymb  14506  s3eqs2s1eq  14861  abssubne0  15240  binom  15753  dvds0lem  16193  dvdsnegb  16200  muldvds1  16207  muldvds2  16208  dvdscmulr  16211  dvdsmulcr  16212  divalgmodcl  16334  gcd2n0cl  16436  gcdaddm  16452  lcmdvds  16535  prmdvdsexp  16642  rpexp1i  16650  monpropd  17661  prfval  18122  xpcpropd  18131  curf2ndf  18170  eqglact  19108  ghmqusker  19216  mndodcongi  19472  oddvdsnn0  19473  efgi0  19649  efgi1  19650  efgsval2  19662  lss0cl  20898  mpofrlmd  21732  evls1fpws  22313  scmatscmid  22450  pmatcollpw3fi1lem1  22730  cnpval  23180  cnf2  23193  cnnei  23226  lfinun  23469  ptpjcn  23555  cnmptk2  23630  flfval  23934  cnmpt2plusg  24032  cnmpt2vsca  24139  ustincl  24152  xbln0  24358  blssec  24379  blpnfctr  24380  mopni2  24437  mopni3  24438  nmoval  24659  nmocl  24664  isnghm2  24668  isnmhm2  24696  cnmpt2ds  24788  metdseq0  24799  cnmpt2ip  25204  caucfil  25239  mbfimasn  25589  dvnf  25885  dvnbss  25886  coemul  26213  dvply1  26247  dvnply2  26251  pserdvlem2  26394  logeftb  26548  advlogexp  26620  cxpne0  26642  cxpp1  26645  elno2  27622  f1otrg  28943  ax5seglem9  29010  uhgrn0  29140  upgrn0  29162  upgrle  29163  uhgrwkspthlem2  29827  frgrhash2wsp  30407  sspval  30798  sspnval  30812  lnof  30830  nmooval  30838  nmooge0  30842  nmoub3i  30848  bloln  30859  nmblore  30861  hosval  31815  homval  31816  hodval  31817  hfsval  31818  hfmval  31819  homulass  31877  hoadddir  31879  nmopub2tALT  31984  nmfnleub2  32001  kbval  32029  lnopmul  32042  0lnfn  32060  lnopcoi  32078  nmcoplb  32105  nmcfnlb  32129  kbass2  32192  nmopleid  32214  hstoh  32307  mdi  32370  dmdi  32377  dmdi4  32382  tpssg  32612  fdifsuppconst  32768  supxrnemnf  32848  elrgspnlem2  33325  rloccring  33352  reofld  33424  nsgmgclem  33492  rhmimaidl  33513  dfufd2lem  33630  r1plmhm  33691  r1pquslmic  33692  lbsdiflsp0  33783  evls1fldgencl  33827  zarclsun  34027  zarclsint  34029  bnj605  35063  bnj607  35072  bnj1097  35137  fnrelpredd  35247  rankfilimb  35258  cusgredgex  35316  topdifinffinlem  37552  lindsdom  37815  lindsenlbs  37816  ftc1anclem2  37895  fzmul  37942  nninfnub  37952  exidreslem  38078  grposnOLD  38083  ghomf  38091  rngohomf  38167  rngohom1  38169  rngohomadd  38170  rngohommul  38171  rngoiso1o  38180  rngoisohom  38181  igenmin  38265  lkrcl  39362  lkrf0  39363  omlfh1N  39528  tendoex  41245  uzindd  42241  primrootsunit1  42361  sticksstones3  42412  sticksstones10  42419  sticksstones12a  42421  sticksstones12  42422  sticksstones17  42427  3anrabdioph  43034  3orrabdioph  43035  rencldnfilem  43072  dvdsabsmod0  43239  jm2.18  43240  jm2.25  43251  jm2.15nn0  43255  tfsconcatlem  43588  onsucunitp  43625  addrfv  44719  subrfv  44720  mulvfv  44721  bi3impa  44736  ssfiunibd  45567  supminfxr  45718  limsupgtlem  46031  xlimmnfv  46088  xlimpnfv  46092  dvnmul  46197  stoweidlem34  46288  stoweidlem48  46302  sge0cl  46635  sge0xp  46683  ovnsubaddlem1  46824  aovmpt4g  47457  gboge9  48020