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  3829  tpssi  3836  sotricim  4413  elirr  4632  en2lp  4645  reg3exmidlemwe  4670  sotri2  5125  poltletr  5128  funprg  5370  funtpg  5371  fntpg  5376  funimaexglem  5403  fvun1  5699  ftpg  5822  fsnunf  5838  fsnunfv  5839  caovimo  6198  brtposg  6398  smoel  6444  rdgivallem  6525  frecsuclem  6550  domssr  6927  mapxpen  7005  unsnfi  7077  unsnfidcex  7078  unsnfidcel  7079  sbthlemi4  7123  elfir  7136  updjud  7245  ltsopi  7503  distrnqg  7570  ltmnqg  7584  mulcanenq0ec  7628  distrnq0  7642  prarloclem5  7683  1idprl  7773  1idpru  7774  ltaprg  7802  recexprlemopl  7808  recexprlemopu  7810  recexprlem1ssl  7816  aptipr  7824  ltmprr  7825  cauappcvgprlemlol  7830  cauappcvgprlemupu  7832  caucvgprlemlol  7853  caucvgprlemupu  7855  caucvgprprlemlol  7881  caucvgprprlemupu  7883  readdcan  8282  cnegexlem2  8318  addcan2  8323  ltadd2  8562  apreap  8730  ltmul1  8735  apcotr  8750  apadd1  8751  mulext1  8755  divdirap  8840  divcanap5  8857  ltdiv1  9011  lt2halves  9343  zdivmul  9533  eluzsub  9748  ledivge1le  9918  addlelt  9960  xaddass  10061  xleadd1  10067  xltadd1  10068  elioo5  10125  iccsupr  10158  iccneg  10181  icoshft  10182  icoshftf1o  10183  zltaddlt1le  10199  fzen  10235  elfz1b  10282  fzrevral  10297  fzshftral  10300  elfz0ubfz0  10317  elfz0fzfz0  10318  fz0fzelfz0  10319  fz0fzdiffz0  10322  elfzo  10341  fzodcel  10345  elfzonlteqm1  10411  modqaddmulmod  10608  expdivap  10807  leexp2a  10809  bcval3  10968  omgadd  11019  ccatval1  11127  ccatval2  11128  ccatval3  11129  ccatass  11138  ccats1val2  11166  swrdval2  11178  swrdlen  11179  pfxfv  11211  pfxnd  11216  pfxsuffeqwrdeq  11225  swrdswrdlem  11231  swrdswrd  11232  pfxswrd  11233  pfxpfx  11235  ccats1pfxeq  11241  ccats1pfxeqrex  11242  pfxccatin12lem2  11258  pfxccatpfx1  11263  swrdccat3b  11267  pfxccatid  11268  shftfibg  11326  elicc4abs  11600  xrmaxltsup  11764  xrmaxadd  11767  xrlemininf  11777  xrminltinf  11778  mulcn2  11818  fsumsplitsnun  11925  prodfrecap  12052  demoivreALT  12280  dvdsval2  12296  dvdsmodexp  12301  dvdsmulcr  12327  modmulconst  12329  dvdsexp  12367  oddge22np1  12387  modremain  12435  mulgcd  12532  mulgcdr  12534  gcddiv  12535  rpmulgcd  12542  rplpwr  12543  coprmdvds  12609  cncongr1  12620  dvdsnprmd  12642  prmexpb  12668  rpexp  12670  cncongrprm  12674  modprm0  12772  modprmn0modprm0  12774  coprimeprodsq  12775  pythagtriplem1  12783  pythagtriplem3  12785  pythagtriplem10  12787  pythagtriplem6  12788  pythagtriplem11  12792  pythagtriplem12  12793  pythagtriplem13  12794  pythagtriplem15  12796  pythagtriplem17  12798  pythagtriplem19  12800  pcdvdsb  12838  dvdsprmpweqle  12855  pcfaclem  12867  isstructr  13042  setsvala  13058  setsresg  13065  strle3g  13136  imasaddvallemg  13343  fvprif  13371  mgmsscl  13389  insubm  13513  dfgrp3mlem  13626  mulgdirlem  13685  mulgp1  13687  mulgmodid  13693  eqglact  13757  rngdi  13898  rngdir  13899  rmodislmodlem  14308  rmodislmod  14309  lssclg  14322  2idlcpblrng  14481  qusmulrng  14490  clsss  14786  ntrcls0  14799  neiss  14818  neipsm  14822  cnpnei  14887  cncnp2m  14899  cnconst2  14901  sslm  14915  upxp  14940  txmetcn  15187  ptolemy  15492  sincosq1eq  15507  rplogbval  15613  rpcxplogb  15632  lgsdirprm  15707  lgsdirnn0  15720  gausslemma2dlem1a  15731  gausslemma2dlem3  15736  2lgslem1a1  15759  2lgsoddprmlem1  15778  2lgsoddprmlem2  15779  structiedg0val  15835  lpvtx  15873  incistruhgr  15884  upgredg2vtx  15940  upgredgpr  15941  ausgrumgrien  15962  ausgrusgrien  15963  ushgredgedg  16018  ushgredgedgloop  16020  wlkvtxeledgg  16041  findset  16266