Theorem 3ad2ant3 1044

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
3ad2ant3	⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantl 277	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜒)
3	2	3adant1 1039	1 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simp3l  1049  simp3r  1050  simp31  1057  simp32  1058  simp33  1059  simp3ll  1092  simp3lr  1093  simp3rl  1094  simp3rr  1095  simp3l1  1126  simp3l2  1127  simp3l3  1128  simp3r1  1129  simp3r2  1130  simp3r3  1131  simp31l  1144  simp31r  1145  simp32l  1146  simp32r  1147  simp33l  1148  simp33r  1149  simp311  1168  simp312  1169  simp313  1170  simp321  1171  simp322  1172  simp323  1173  simp331  1174  simp332  1175  simp333  1176  3anim123i  1208  3jaao  1342  ceqsalt  2826  ceqsralt  2827  vtoclgft  2851  ifbothdc  3637  ifnebibdc  3648  ssprsseq  3830  tpssi  3837  sotricim  4414  elirr  4633  en2lp  4646  reg3exmidlemwe  4671  sotri2  5126  poltletr  5129  funprg  5371  funtpg  5372  fntpg  5377  funimaexglem  5404  fvun1  5702  ftpg  5827  fsnunf  5843  fsnunfv  5844  caovimo  6205  brtposg  6406  smoel  6452  rdgivallem  6533  frecsuclem  6558  domssr  6937  mapxpen  7017  unsnfi  7089  unsnfidcex  7090  unsnfidcel  7091  sbthlemi4  7135  elfir  7148  updjud  7257  ltsopi  7515  distrnqg  7582  ltmnqg  7596  mulcanenq0ec  7640  distrnq0  7654  prarloclem5  7695  1idprl  7785  1idpru  7786  ltaprg  7814  recexprlemopl  7820  recexprlemopu  7822  recexprlem1ssl  7828  aptipr  7836  ltmprr  7837  cauappcvgprlemlol  7842  cauappcvgprlemupu  7844  caucvgprlemlol  7865  caucvgprlemupu  7867  caucvgprprlemlol  7893  caucvgprprlemupu  7895  readdcan  8294  cnegexlem2  8330  addcan2  8335  ltadd2  8574  apreap  8742  ltmul1  8747  apcotr  8762  apadd1  8763  mulext1  8767  divdirap  8852  divcanap5  8869  ltdiv1  9023  lt2halves  9355  zdivmul  9545  eluzsub  9760  ledivge1le  9930  addlelt  9972  xaddass  10073  xleadd1  10079  xltadd1  10080  elioo5  10137  iccsupr  10170  iccneg  10193  icoshft  10194  icoshftf1o  10195  zltaddlt1le  10211  fzen  10247  elfz1b  10294  fzrevral  10309  fzshftral  10312  elfz0ubfz0  10329  elfz0fzfz0  10330  fz0fzelfz0  10331  fz0fzdiffz0  10334  elfzo  10353  fzodcel  10357  elfzonlteqm1  10424  modqaddmulmod  10621  expdivap  10820  leexp2a  10822  bcval3  10981  omgadd  11032  ccatval1  11140  ccatval2  11141  ccatval3  11142  ccatass  11151  ccats1val2  11179  swrdval2  11191  swrdlen  11192  pfxfv  11224  pfxnd  11229  pfxsuffeqwrdeq  11238  swrdswrdlem  11244  swrdswrd  11245  pfxswrd  11246  pfxpfx  11248  ccats1pfxeq  11254  ccats1pfxeqrex  11255  pfxccatin12lem2  11271  pfxccatpfx1  11276  swrdccat3b  11280  pfxccatid  11281  shftfibg  11339  elicc4abs  11613  xrmaxltsup  11777  xrmaxadd  11780  xrlemininf  11790  xrminltinf  11791  mulcn2  11831  fsumsplitsnun  11938  prodfrecap  12065  demoivreALT  12293  dvdsval2  12309  dvdsmodexp  12314  dvdsmulcr  12340  modmulconst  12342  dvdsexp  12380  oddge22np1  12400  modremain  12448  mulgcd  12545  mulgcdr  12547  gcddiv  12548  rpmulgcd  12555  rplpwr  12556  coprmdvds  12622  cncongr1  12633  dvdsnprmd  12655  prmexpb  12681  rpexp  12683  cncongrprm  12687  modprm0  12785  modprmn0modprm0  12787  coprimeprodsq  12788  pythagtriplem1  12796  pythagtriplem3  12798  pythagtriplem10  12800  pythagtriplem6  12801  pythagtriplem11  12805  pythagtriplem12  12806  pythagtriplem13  12807  pythagtriplem15  12809  pythagtriplem17  12811  pythagtriplem19  12813  pcdvdsb  12851  dvdsprmpweqle  12868  pcfaclem  12880  isstructr  13055  setsvala  13071  setsresg  13078  strle3g  13149  imasaddvallemg  13356  fvprif  13384  mgmsscl  13402  insubm  13526  dfgrp3mlem  13639  mulgdirlem  13698  mulgp1  13700  mulgmodid  13706  eqglact  13770  rngdi  13911  rngdir  13912  rmodislmodlem  14322  rmodislmod  14323  lssclg  14336  2idlcpblrng  14495  qusmulrng  14504  clsss  14800  ntrcls0  14813  neiss  14832  neipsm  14836  cnpnei  14901  cncnp2m  14913  cnconst2  14915  sslm  14929  upxp  14954  txmetcn  15201  ptolemy  15506  sincosq1eq  15521  rplogbval  15627  rpcxplogb  15646  lgsdirprm  15721  lgsdirnn0  15734  gausslemma2dlem1a  15745  gausslemma2dlem3  15750  2lgslem1a1  15773  2lgsoddprmlem1  15792  2lgsoddprmlem2  15793  structiedg0val  15849  lpvtx  15887  incistruhgr  15898  upgredg2vtx  15954  upgredgpr  15955  ausgrumgrien  15976  ausgrusgrien  15977  ushgredgedg  16032  ushgredgedgloop  16034  wlkvtxeledgg  16065  wlkeq  16075  wlkl1loop  16079  uspgr2wlkeq  16086  uspgr2wlkeq2  16087  wlkres  16098  findset  16332