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  7092  unsnfidcex  7093  unsnfidcel  7094  sbthlemi4  7138  elfir  7151  updjud  7260  ltsopi  7518  distrnqg  7585  ltmnqg  7599  mulcanenq0ec  7643  distrnq0  7657  prarloclem5  7698  1idprl  7788  1idpru  7789  ltaprg  7817  recexprlemopl  7823  recexprlemopu  7825  recexprlem1ssl  7831  aptipr  7839  ltmprr  7840  cauappcvgprlemlol  7845  cauappcvgprlemupu  7847  caucvgprlemlol  7868  caucvgprlemupu  7870  caucvgprprlemlol  7896  caucvgprprlemupu  7898  readdcan  8297  cnegexlem2  8333  addcan2  8338  ltadd2  8577  apreap  8745  ltmul1  8750  apcotr  8765  apadd1  8766  mulext1  8770  divdirap  8855  divcanap5  8872  ltdiv1  9026  lt2halves  9358  zdivmul  9548  eluzsub  9764  ledivge1le  9934  addlelt  9976  xaddass  10077  xleadd1  10083  xltadd1  10084  elioo5  10141  iccsupr  10174  iccneg  10197  icoshft  10198  icoshftf1o  10199  zltaddlt1le  10215  fzen  10251  elfz1b  10298  fzrevral  10313  fzshftral  10316  elfz0ubfz0  10333  elfz0fzfz0  10334  fz0fzelfz0  10335  fz0fzdiffz0  10338  elfzo  10357  fzodcel  10361  elfzonlteqm1  10428  modqaddmulmod  10625  expdivap  10824  leexp2a  10826  bcval3  10985  omgadd  11036  ccatval1  11145  ccatval2  11146  ccatval3  11147  ccatass  11156  ccats1val2  11186  swrdval2  11198  swrdlen  11199  pfxfv  11231  pfxnd  11236  pfxsuffeqwrdeq  11245  swrdswrdlem  11251  swrdswrd  11252  pfxswrd  11253  pfxpfx  11255  ccats1pfxeq  11261  ccats1pfxeqrex  11262  pfxccatin12lem2  11278  pfxccatpfx1  11283  swrdccat3b  11287  pfxccatid  11288  shftfibg  11346  elicc4abs  11620  xrmaxltsup  11784  xrmaxadd  11787  xrlemininf  11797  xrminltinf  11798  mulcn2  11838  fsumsplitsnun  11945  prodfrecap  12072  demoivreALT  12300  dvdsval2  12316  dvdsmodexp  12321  dvdsmulcr  12347  modmulconst  12349  dvdsexp  12387  oddge22np1  12407  modremain  12455  mulgcd  12552  mulgcdr  12554  gcddiv  12555  rpmulgcd  12562  rplpwr  12563  coprmdvds  12629  cncongr1  12640  dvdsnprmd  12662  prmexpb  12688  rpexp  12690  cncongrprm  12694  modprm0  12792  modprmn0modprm0  12794  coprimeprodsq  12795  pythagtriplem1  12803  pythagtriplem3  12805  pythagtriplem10  12807  pythagtriplem6  12808  pythagtriplem11  12812  pythagtriplem12  12813  pythagtriplem13  12814  pythagtriplem15  12816  pythagtriplem17  12818  pythagtriplem19  12820  pcdvdsb  12858  dvdsprmpweqle  12875  pcfaclem  12887  isstructr  13062  setsvala  13078  setsresg  13085  strle3g  13156  imasaddvallemg  13363  fvprif  13391  mgmsscl  13409  insubm  13533  dfgrp3mlem  13646  mulgdirlem  13705  mulgp1  13707  mulgmodid  13713  eqglact  13777  rngdi  13918  rngdir  13919  rmodislmodlem  14329  rmodislmod  14330  lssclg  14343  2idlcpblrng  14502  qusmulrng  14511  clsss  14807  ntrcls0  14820  neiss  14839  neipsm  14843  cnpnei  14908  cncnp2m  14920  cnconst2  14922  sslm  14936  upxp  14961  txmetcn  15208  ptolemy  15513  sincosq1eq  15528  rplogbval  15634  rpcxplogb  15653  lgsdirprm  15728  lgsdirnn0  15741  gausslemma2dlem1a  15752  gausslemma2dlem3  15757  2lgslem1a1  15780  2lgsoddprmlem1  15799  2lgsoddprmlem2  15800  structiedg0val  15856  lpvtx  15894  incistruhgr  15905  upgredg2vtx  15961  upgredgpr  15962  ausgrumgrien  15983  ausgrusgrien  15984  ushgredgedg  16039  ushgredgedgloop  16041  wlkvtxeledgg  16085  wlkeq  16095  wlkl1loop  16099  uspgr2wlkeq  16106  uspgr2wlkeq2  16107  wlkres  16118  findset  16363