Theorem 3ad2ant2 1003

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 274	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3	2	3adant1 999	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simp2l  1007  simp2r  1008  simp21  1014  simp22  1015  simp23  1016  simp2ll  1048  simp2lr  1049  simp2rl  1050  simp2rr  1051  simp2l1  1080  simp2l2  1081  simp2l3  1082  simp2r1  1083  simp2r2  1084  simp2r3  1085  simp21l  1098  simp21r  1099  simp22l  1100  simp22r  1101  simp23l  1102  simp23r  1103  simp211  1119  simp212  1120  simp213  1121  simp221  1122  simp222  1123  simp223  1124  simp231  1125  simp232  1126  simp233  1127  3anim123i  1166  3jaao  1286  ceqsalt  2707  vtoclgft  2731  vtoclegft  2753  ifbothdc  3499  frirrg  4267  elirr  4451  en2lp  4464  reg3exmidlemwe  4488  sotri3  4932  funtpg  5169  fnprg  5173  fntpg  5174  funimaexglem  5201  fnco  5226  fvun1  5480  oprssov  5905  caovimo  5957  rdgivallem  6271  fnsnsplitdc  6394  funresdfunsndc  6395  f1dom2g  6643  mapxpen  6735  ssfidc  6816  sbthlemi4  6841  ordiso2  6913  updjud  6960  difinfsn  6978  mkvprop  7025  endjudisj  7059  distrnqg  7188  distrnq0  7260  prarloclem5  7301  cauappcvgprlemlol  7448  cauappcvgprlemupu  7450  caucvgprlemlol  7471  caucvgprlemupu  7473  caucvgprprlemlol  7499  caucvgprprlemupu  7501  cnegexlem2  7931  apcotr  8362  apadd1  8363  mulext1  8367  div2negap  8488  ltdiv2  8638  nndivtr  8755  zdivmul  9134  gtndiv  9139  fzind  9159  eluzuzle  9327  eluzp1p1  9344  peano2uz  9371  qdivcl  9428  irrmul  9432  ledivge1le  9506  xrre2  9597  xaddass  9645  xltadd1  9652  xlt2add  9656  ubioc1  9705  ubicc2  9761  zltaddlt1le  9782  uzsubsubfz  9820  elfz1b  9863  fzp1nel  9877  fz0fzdiffz0  9900  difelfzle  9904  elfzo0  9952  elfzonlteqm1  9980  fzonn0p1p1  9983  fzosplitprm1  10004  fzoshftral  10008  subfzo0  10012  ceiqle  10079  modqval  10090  modqvalr  10091  flqpmodeq  10093  modq0  10095  mulqmod0  10096  negqmod0  10097  modqge0  10098  modqlt  10099  modqelico  10100  modqdiffl  10101  modqmulnn  10108  modqvalp1  10109  modqmuladdnn0  10134  qnegmod  10135  addmodid  10138  q2submod  10151  modifeq2int  10152  modfzo0difsn  10161  addmodlteq  10164  omgadd  10541  hashun  10544  redivap  10639  imdivap  10646  xrmaxltsup  11020  xrmaxadd  11023  xrlemininf  11033  xrminltinf  11034  climuni  11055  mulcn2  11074  fsumsplitsnun  11181  prodfap0  11307  efsub  11376  cos12dec  11463  summodnegmod  11513  divalglemex  11608  divalg  11610  modremain  11615  ndvdssub  11616  fldivndvdslt  11621  nndvdslegcd  11643  dfgcd2  11691  mulgcd  11693  mulgcdr  11695  gcddiv  11696  rplpwr  11704  rppwr  11705  qredeq  11766  divgcdcoprmex  11772  cncongr1  11773  cncongr2  11774  pw2dvdslemn  11832  hashgcdlem  11892  unennn  11899  ntrin  12282  elnei  12310  restco  12332  cnpnei  12377  cncnp2m  12389  sslm  12405  upxp  12430  blres  12592  metcnp3  12669  tgqioo  12705  ptolemy  12894