Theorem 3ad2ant2 1019

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3	2	3adant1 1015	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  simp2l  1023  simp2r  1024  simp21  1030  simp22  1031  simp23  1032  simp2ll  1064  simp2lr  1065  simp2rl  1066  simp2rr  1067  simp2l1  1096  simp2l2  1097  simp2l3  1098  simp2r1  1099  simp2r2  1100  simp2r3  1101  simp21l  1114  simp21r  1115  simp22l  1116  simp22r  1117  simp23l  1118  simp23r  1119  simp211  1135  simp212  1136  simp213  1137  simp221  1138  simp222  1139  simp223  1140  simp231  1141  simp232  1142  simp233  1143  3anim123i  1184  3jaao  1308  ceqsalt  2764  vtoclgft  2788  vtoclegft  2810  ifbothdc  3568  frirrg  4351  elirr  4541  en2lp  4554  reg3exmidlemwe  4579  sotri3  5028  funtpg  5268  fnprg  5272  fntpg  5273  funimaexglem  5300  fnco  5325  fvun1  5583  oprssov  6016  caovimo  6068  rdgivallem  6382  fnsnsplitdc  6506  funresdfunsndc  6507  f1dom2g  6756  mapxpen  6848  ssfidc  6934  sbthlemi4  6959  ordiso2  7034  updjud  7081  difinfsn  7099  mkvprop  7156  endjudisj  7209  distrnqg  7386  distrnq0  7458  prarloclem5  7499  cauappcvgprlemlol  7646  cauappcvgprlemupu  7648  caucvgprlemlol  7669  caucvgprlemupu  7671  caucvgprprlemlol  7697  caucvgprprlemupu  7699  cnegexlem2  8133  apcotr  8564  apadd1  8565  mulext1  8569  div2negap  8692  ltdiv2  8844  nndivtr  8961  difgtsumgt  9322  zdivmul  9343  gtndiv  9348  fzind  9368  eluzuzle  9536  eluzp1p1  9553  peano2uz  9583  qdivcl  9643  irrmul  9647  ledivge1le  9726  xrre2  9821  xaddass  9869  xltadd1  9876  xlt2add  9880  ubioc1  9929  ubicc2  9985  zltaddlt1le  10007  uzsubsubfz  10047  elfz1b  10090  fzp1nel  10104  fz0fzdiffz0  10130  difelfzle  10134  elfzo0  10182  elfzonlteqm1  10210  fzonn0p1p1  10213  fzosplitprm1  10234  fzoshftral  10238  subfzo0  10242  ceiqle  10313  modqval  10324  modqvalr  10325  flqpmodeq  10327  modq0  10329  mulqmod0  10330  negqmod0  10331  modqge0  10332  modqlt  10333  modqelico  10334  modqdiffl  10335  modqmulnn  10342  modqvalp1  10343  modqmuladdnn0  10368  qnegmod  10369  addmodid  10372  q2submod  10385  modifeq2int  10386  modfzo0difsn  10395  addmodlteq  10398  mulsubdivbinom2ap  10691  omgadd  10782  hashun  10785  redivap  10883  imdivap  10890  xrmaxltsup  11266  xrmaxadd  11269  xrlemininf  11279  xrminltinf  11280  climuni  11301  mulcn2  11320  fsumsplitsnun  11427  prodfap0  11553  fprodabs  11624  efsub  11689  cos12dec  11775  dvdsmodexp  11802  summodnegmod  11829  divalglemex  11927  divalg  11929  modremain  11934  ndvdssub  11935  fldivndvdslt  11940  nndvdslegcd  11966  dfgcd2  12015  mulgcd  12017  mulgcdr  12019  gcddiv  12020  rplpwr  12028  rppwr  12029  qredeq  12096  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  pw2dvdslemn  12165  hashgcdlem  12238  modprm0  12254  modprmn0modprm0  12256  pythagtriplem1  12265  pythagtriplem3  12267  pythagtriplem10  12269  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem11  12274  pythagtriplem12  12275  pythagtriplem13  12276  pythagtriplem14  12277  pythagtriplem19  12282  pythagtrip  12283  dvdsprmpweqnn  12335  difsqpwdvds  12337  pcfaclem  12347  pcbc  12349  unennn  12398  ptex  12713  imasaddvallemg  12736  fvprif  12762  mgmsscl  12780  insubm  12872  mulginvcom  13008  mulgassr  13021  mulgmodid  13022  rmodislmodlem  13440  rmodislmod  13441  ntrin  13627  elnei  13655  restco  13677  cnpnei  13722  cncnp2m  13734  sslm  13750  upxp  13775  blres  13937  metcnp3  14014  tgqioo  14050  ptolemy  14248  cxpcom  14360  logbgcd1irr  14388  logbprmirr  14393  lgslem1  14404  lgsneg  14428  lgsdilem  14431  lgsdir  14439  lgssq2  14445  lgsdirnn0  14451