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  2765  vtoclgft  2789  vtoclegft  2811  ifbothdc  3569  frirrg  4352  elirr  4542  en2lp  4555  reg3exmidlemwe  4580  sotri3  5029  funtpg  5269  fnprg  5273  fntpg  5274  funimaexglem  5301  fnco  5326  fvun1  5584  oprssov  6018  caovimo  6070  rdgivallem  6384  fnsnsplitdc  6508  funresdfunsndc  6509  f1dom2g  6758  mapxpen  6850  ssfidc  6936  sbthlemi4  6961  ordiso2  7036  updjud  7083  difinfsn  7101  mkvprop  7158  endjudisj  7211  distrnqg  7388  distrnq0  7460  prarloclem5  7501  cauappcvgprlemlol  7648  cauappcvgprlemupu  7650  caucvgprlemlol  7671  caucvgprlemupu  7673  caucvgprprlemlol  7699  caucvgprprlemupu  7701  cnegexlem2  8135  apcotr  8566  apadd1  8567  mulext1  8571  div2negap  8694  ltdiv2  8846  nndivtr  8963  difgtsumgt  9324  zdivmul  9345  gtndiv  9350  fzind  9370  eluzuzle  9538  eluzp1p1  9555  peano2uz  9585  qdivcl  9645  irrmul  9649  ledivge1le  9728  xrre2  9823  xaddass  9871  xltadd1  9878  xlt2add  9882  ubioc1  9931  ubicc2  9987  zltaddlt1le  10009  uzsubsubfz  10049  elfz1b  10092  fzp1nel  10106  fz0fzdiffz0  10132  difelfzle  10136  elfzo0  10184  elfzonlteqm1  10212  fzonn0p1p1  10215  fzosplitprm1  10236  fzoshftral  10240  subfzo0  10244  ceiqle  10315  modqval  10326  modqvalr  10327  flqpmodeq  10329  modq0  10331  mulqmod0  10332  negqmod0  10333  modqge0  10334  modqlt  10335  modqelico  10336  modqdiffl  10337  modqmulnn  10344  modqvalp1  10345  modqmuladdnn0  10370  qnegmod  10371  addmodid  10374  q2submod  10387  modifeq2int  10388  modfzo0difsn  10397  addmodlteq  10400  mulsubdivbinom2ap  10693  omgadd  10784  hashun  10787  redivap  10885  imdivap  10892  xrmaxltsup  11268  xrmaxadd  11271  xrlemininf  11281  xrminltinf  11282  climuni  11303  mulcn2  11322  fsumsplitsnun  11429  prodfap0  11555  fprodabs  11626  efsub  11691  cos12dec  11777  dvdsmodexp  11804  summodnegmod  11831  divalglemex  11929  divalg  11931  modremain  11936  ndvdssub  11937  fldivndvdslt  11942  nndvdslegcd  11968  dfgcd2  12017  mulgcd  12019  mulgcdr  12021  gcddiv  12022  rplpwr  12030  rppwr  12031  qredeq  12098  divgcdcoprmex  12104  cncongr1  12105  cncongr2  12106  pw2dvdslemn  12167  hashgcdlem  12240  modprm0  12256  modprmn0modprm0  12258  pythagtriplem1  12267  pythagtriplem3  12269  pythagtriplem10  12271  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem11  12276  pythagtriplem12  12277  pythagtriplem13  12278  pythagtriplem14  12279  pythagtriplem19  12284  pythagtrip  12285  dvdsprmpweqnn  12337  difsqpwdvds  12339  pcfaclem  12349  pcbc  12351  unennn  12400  ptex  12718  imasaddvallemg  12741  fvprif  12767  mgmsscl  12785  insubm  12877  mulginvcom  13013  mulgassr  13026  mulgmodid  13027  rmodislmodlem  13445  rmodislmod  13446  lssincl  13477  ntrin  13663  elnei  13691  restco  13713  cnpnei  13758  cncnp2m  13770  sslm  13786  upxp  13811  blres  13973  metcnp3  14050  tgqioo  14086  ptolemy  14284  cxpcom  14396  logbgcd1irr  14424  logbprmirr  14429  lgslem1  14440  lgsneg  14464  lgsdilem  14467  lgsdir  14475  lgssq2  14481  lgsdirnn0  14487