Theorem 3ad2ant2 971

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

Syntax hints:   → wi 4   ∧ w3a 930

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

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

This theorem is referenced by:  simp2l  975  simp2r  976  simp21  982  simp22  983  simp23  984  simp2ll  1016  simp2lr  1017  simp2rl  1018  simp2rr  1019  simp2l1  1048  simp2l2  1049  simp2l3  1050  simp2r1  1051  simp2r2  1052  simp2r3  1053  simp21l  1066  simp21r  1067  simp22l  1068  simp22r  1069  simp23l  1070  simp23r  1071  simp211  1087  simp212  1088  simp213  1089  simp221  1090  simp222  1091  simp223  1092  simp231  1093  simp232  1094  simp233  1095  3anim123i  1134  3jaao  1254  ceqsalt  2667  vtoclgft  2691  vtoclegft  2713  ifbothdc  3451  frirrg  4210  elirr  4394  en2lp  4407  reg3exmidlemwe  4431  sotri3  4873  funtpg  5110  fnprg  5114  fntpg  5115  funimaexglem  5142  fnco  5167  fvun1  5419  oprssov  5844  caovimo  5896  rdgivallem  6208  fnsnsplitdc  6331  funresdfunsndc  6332  f1dom2g  6580  mapxpen  6671  ssfidc  6751  sbthlemi4  6776  ordiso2  6835  updjud  6882  difinfsn  6900  mkvprop  6943  endjudisj  6970  distrnqg  7096  distrnq0  7168  prarloclem5  7209  cauappcvgprlemlol  7356  cauappcvgprlemupu  7358  caucvgprlemlol  7379  caucvgprlemupu  7381  caucvgprprlemlol  7407  caucvgprprlemupu  7409  cnegexlem2  7809  apcotr  8235  apadd1  8236  mulext1  8240  div2negap  8356  ltdiv2  8503  nndivtr  8620  zdivmul  8993  gtndiv  8998  fzind  9018  eluzuzle  9184  eluzp1p1  9201  peano2uz  9228  qdivcl  9285  irrmul  9289  ledivge1le  9360  xrre2  9445  xaddass  9493  xltadd1  9500  xlt2add  9504  ubioc1  9553  ubicc2  9609  zltaddlt1le  9630  uzsubsubfz  9668  elfz1b  9711  fzp1nel  9725  fz0fzdiffz0  9748  difelfzle  9752  elfzo0  9800  elfzonlteqm1  9828  fzonn0p1p1  9831  fzosplitprm1  9852  fzoshftral  9856  subfzo0  9860  ceiqle  9927  modqval  9938  modqvalr  9939  flqpmodeq  9941  modq0  9943  mulqmod0  9944  negqmod0  9945  modqge0  9946  modqlt  9947  modqelico  9948  modqdiffl  9949  modqmulnn  9956  modqvalp1  9957  modqmuladdnn0  9982  qnegmod  9983  addmodid  9986  q2submod  9999  modifeq2int  10000  modfzo0difsn  10009  addmodlteq  10012  omgadd  10389  hashun  10392  redivap  10487  imdivap  10494  xrmaxltsup  10866  xrmaxadd  10869  xrlemininf  10879  xrminltinf  10880  climuni  10901  mulcn2  10920  fsumsplitsnun  11027  efsub  11185  summodnegmod  11319  divalglemex  11414  divalg  11416  modremain  11421  ndvdssub  11422  fldivndvdslt  11427  nndvdslegcd  11449  dfgcd2  11495  mulgcd  11497  mulgcdr  11499  gcddiv  11500  rplpwr  11508  rppwr  11509  qredeq  11570  divgcdcoprmex  11576  cncongr1  11577  cncongr2  11578  pw2dvdslemn  11635  hashgcdlem  11695  unennn  11702  ntrin  12075  elnei  12103  restco  12125  cnpnei  12169  cncnp2m  12181  sslm  12197  upxp  12222  blres  12362  metcnp3  12435  tgqioo  12466