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  2763  vtoclgft  2787  vtoclegft  2809  ifbothdc  3567  frirrg  4348  elirr  4538  en2lp  4551  reg3exmidlemwe  4576  sotri3  5024  funtpg  5264  fnprg  5268  fntpg  5269  funimaexglem  5296  fnco  5321  fvun1  5579  oprssov  6011  caovimo  6063  rdgivallem  6377  fnsnsplitdc  6501  funresdfunsndc  6502  f1dom2g  6751  mapxpen  6843  ssfidc  6929  sbthlemi4  6954  ordiso2  7029  updjud  7076  difinfsn  7094  mkvprop  7151  endjudisj  7204  distrnqg  7381  distrnq0  7453  prarloclem5  7494  cauappcvgprlemlol  7641  cauappcvgprlemupu  7643  caucvgprlemlol  7664  caucvgprlemupu  7666  caucvgprprlemlol  7692  caucvgprprlemupu  7694  cnegexlem2  8127  apcotr  8558  apadd1  8559  mulext1  8563  div2negap  8686  ltdiv2  8838  nndivtr  8955  difgtsumgt  9316  zdivmul  9337  gtndiv  9342  fzind  9362  eluzuzle  9530  eluzp1p1  9547  peano2uz  9577  qdivcl  9637  irrmul  9641  ledivge1le  9720  xrre2  9815  xaddass  9863  xltadd1  9870  xlt2add  9874  ubioc1  9923  ubicc2  9979  zltaddlt1le  10001  uzsubsubfz  10040  elfz1b  10083  fzp1nel  10097  fz0fzdiffz0  10123  difelfzle  10127  elfzo0  10175  elfzonlteqm1  10203  fzonn0p1p1  10206  fzosplitprm1  10227  fzoshftral  10231  subfzo0  10235  ceiqle  10306  modqval  10317  modqvalr  10318  flqpmodeq  10320  modq0  10322  mulqmod0  10323  negqmod0  10324  modqge0  10325  modqlt  10326  modqelico  10327  modqdiffl  10328  modqmulnn  10335  modqvalp1  10336  modqmuladdnn0  10361  qnegmod  10362  addmodid  10365  q2submod  10378  modifeq2int  10379  modfzo0difsn  10388  addmodlteq  10391  omgadd  10773  hashun  10776  redivap  10874  imdivap  10881  xrmaxltsup  11257  xrmaxadd  11260  xrlemininf  11270  xrminltinf  11271  climuni  11292  mulcn2  11311  fsumsplitsnun  11418  prodfap0  11544  fprodabs  11615  efsub  11680  cos12dec  11766  dvdsmodexp  11793  summodnegmod  11820  divalglemex  11917  divalg  11919  modremain  11924  ndvdssub  11925  fldivndvdslt  11930  nndvdslegcd  11956  dfgcd2  12005  mulgcd  12007  mulgcdr  12009  gcddiv  12010  rplpwr  12018  rppwr  12019  qredeq  12086  divgcdcoprmex  12092  cncongr1  12093  cncongr2  12094  pw2dvdslemn  12155  hashgcdlem  12228  modprm0  12244  modprmn0modprm0  12246  pythagtriplem1  12255  pythagtriplem3  12257  pythagtriplem10  12259  pythagtriplem6  12260  pythagtriplem7  12261  pythagtriplem11  12264  pythagtriplem12  12265  pythagtriplem13  12266  pythagtriplem14  12267  pythagtriplem19  12272  pythagtrip  12273  dvdsprmpweqnn  12325  difsqpwdvds  12327  pcfaclem  12337  pcbc  12339  unennn  12388  mgmsscl  12710  insubm  12800  mulginvcom  12935  mulgassr  12948  mulgmodid  12949  ntrin  13439  elnei  13467  restco  13489  cnpnei  13534  cncnp2m  13546  sslm  13562  upxp  13587  blres  13749  metcnp3  13826  tgqioo  13862  ptolemy  14060  cxpcom  14172  logbgcd1irr  14200  logbprmirr  14205  lgslem1  14216  lgsneg  14240  lgsdilem  14243  lgsdir  14251  lgssq2  14257  lgsdirnn0  14263