Theorem 3ad2ant2 1020

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 1016	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 979

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 981

This theorem is referenced by:  simp2l  1024  simp2r  1025  simp21  1031  simp22  1032  simp23  1033  simp2ll  1065  simp2lr  1066  simp2rl  1067  simp2rr  1068  simp2l1  1097  simp2l2  1098  simp2l3  1099  simp2r1  1100  simp2r2  1101  simp2r3  1102  simp21l  1115  simp21r  1116  simp22l  1117  simp22r  1118  simp23l  1119  simp23r  1120  simp211  1136  simp212  1137  simp213  1138  simp221  1139  simp222  1140  simp223  1141  simp231  1142  simp232  1143  simp233  1144  3anim123i  1185  3jaao  1318  ceqsalt  2775  vtoclgft  2799  vtoclegft  2821  ifbothdc  3579  frirrg  4362  elirr  4552  en2lp  4565  reg3exmidlemwe  4590  sotri3  5039  funtpg  5279  fnprg  5283  fntpg  5284  funimaexglem  5311  fnco  5336  fvun1  5595  oprssov  6030  caovimo  6082  rdgivallem  6396  fnsnsplitdc  6520  funresdfunsndc  6521  f1dom2g  6770  mapxpen  6862  ssfidc  6948  sbthlemi4  6973  ordiso2  7048  updjud  7095  difinfsn  7113  mkvprop  7170  endjudisj  7223  distrnqg  7400  distrnq0  7472  prarloclem5  7513  cauappcvgprlemlol  7660  cauappcvgprlemupu  7662  caucvgprlemlol  7683  caucvgprlemupu  7685  caucvgprprlemlol  7711  caucvgprprlemupu  7713  cnegexlem2  8147  apcotr  8578  apadd1  8579  mulext1  8583  div2negap  8706  ltdiv2  8858  nndivtr  8975  difgtsumgt  9336  zdivmul  9357  gtndiv  9362  fzind  9382  eluzuzle  9550  eluzp1p1  9567  peano2uz  9597  qdivcl  9657  irrmul  9661  ledivge1le  9740  xrre2  9835  xaddass  9883  xltadd1  9890  xlt2add  9894  ubioc1  9943  ubicc2  9999  zltaddlt1le  10021  uzsubsubfz  10061  elfz1b  10104  fzp1nel  10118  fz0fzdiffz0  10144  difelfzle  10148  elfzo0  10196  elfzonlteqm1  10224  fzonn0p1p1  10227  fzosplitprm1  10248  fzoshftral  10252  subfzo0  10256  ceiqle  10327  modqval  10338  modqvalr  10339  flqpmodeq  10341  modq0  10343  mulqmod0  10344  negqmod0  10345  modqge0  10346  modqlt  10347  modqelico  10348  modqdiffl  10349  modqmulnn  10356  modqvalp1  10357  modqmuladdnn0  10382  qnegmod  10383  addmodid  10386  q2submod  10399  modifeq2int  10400  modfzo0difsn  10409  addmodlteq  10412  mulsubdivbinom2ap  10705  omgadd  10796  hashun  10799  redivap  10897  imdivap  10904  xrmaxltsup  11280  xrmaxadd  11283  xrlemininf  11293  xrminltinf  11294  climuni  11315  mulcn2  11334  fsumsplitsnun  11441  prodfap0  11567  fprodabs  11638  efsub  11703  cos12dec  11789  dvdsmodexp  11816  summodnegmod  11843  divalglemex  11941  divalg  11943  modremain  11948  ndvdssub  11949  fldivndvdslt  11954  nndvdslegcd  11980  dfgcd2  12029  mulgcd  12031  mulgcdr  12033  gcddiv  12034  rplpwr  12042  rppwr  12043  qredeq  12110  divgcdcoprmex  12116  cncongr1  12117  cncongr2  12118  pw2dvdslemn  12179  hashgcdlem  12252  modprm0  12268  modprmn0modprm0  12270  pythagtriplem1  12279  pythagtriplem3  12281  pythagtriplem10  12283  pythagtriplem6  12284  pythagtriplem7  12285  pythagtriplem11  12288  pythagtriplem12  12289  pythagtriplem13  12290  pythagtriplem14  12291  pythagtriplem19  12296  pythagtrip  12297  dvdsprmpweqnn  12349  difsqpwdvds  12351  pcfaclem  12361  pcbc  12363  unennn  12412  ptex  12731  imasaddvallemg  12754  fvprif  12781  mgmsscl  12799  insubm  12894  mulginvcom  13040  mulgassr  13053  mulgmodid  13054  ringrng  13288  rmodislmodlem  13539  rmodislmod  13540  lssincl  13574  sralmod  13639  rnglidlmmgm  13685  rnglidlmsgrp  13686  rnglidlrng  13687  2idlcpblrng  13711  ntrin  13920  elnei  13948  restco  13970  cnpnei  14015  cncnp2m  14027  sslm  14043  upxp  14068  blres  14230  metcnp3  14307  tgqioo  14343  ptolemy  14541  cxpcom  14653  logbgcd1irr  14681  logbprmirr  14686  lgslem1  14697  lgsneg  14721  lgsdilem  14724  lgsdir  14732  lgssq2  14738  lgsdirnn0  14744