Theorem 3ad2ant2 1021

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp2l  1025  simp2r  1026  simp21  1032  simp22  1033  simp23  1034  simp2ll  1066  simp2lr  1067  simp2rl  1068  simp2rr  1069  simp2l1  1098  simp2l2  1099  simp2l3  1100  simp2r1  1101  simp2r2  1102  simp2r3  1103  simp21l  1116  simp21r  1117  simp22l  1118  simp22r  1119  simp23l  1120  simp23r  1121  simp211  1137  simp212  1138  simp213  1139  simp221  1140  simp222  1141  simp223  1142  simp231  1143  simp232  1144  simp233  1145  3anim123i  1186  3jaao  1319  ceqsalt  2786  vtoclgft  2810  vtoclegft  2832  ifbothdc  3590  ifnebibdc  3600  frirrg  4381  elirr  4573  en2lp  4586  reg3exmidlemwe  4611  sotri3  5064  funtpg  5305  fnprg  5309  fntpg  5310  funimaexglem  5337  fnco  5362  fvun1  5623  oprssov  6060  caovimo  6112  rdgivallem  6434  fnsnsplitdc  6558  funresdfunsndc  6559  f1dom2g  6810  mapxpen  6904  ssfidc  6991  sbthlemi4  7019  ordiso2  7094  updjud  7141  difinfsn  7159  mkvprop  7217  endjudisj  7270  distrnqg  7447  distrnq0  7519  prarloclem5  7560  cauappcvgprlemlol  7707  cauappcvgprlemupu  7709  caucvgprlemlol  7730  caucvgprlemupu  7732  caucvgprprlemlol  7758  caucvgprprlemupu  7760  cnegexlem2  8195  apcotr  8626  apadd1  8627  mulext1  8631  div2negap  8754  ltdiv2  8906  nndivtr  9024  difgtsumgt  9386  zdivmul  9407  gtndiv  9412  fzind  9432  eluzuzle  9600  eluzp1p1  9618  peano2uz  9648  qdivcl  9708  irrmul  9712  ledivge1le  9792  xrre2  9887  xaddass  9935  xltadd1  9942  xlt2add  9946  ubioc1  9995  ubicc2  10051  zltaddlt1le  10073  uzsubsubfz  10113  elfz1b  10156  fzp1nel  10170  fz0fzdiffz0  10196  difelfzle  10200  elfzo0  10249  elfzonlteqm1  10277  fzonn0p1p1  10280  fzosplitprm1  10301  fzoshftral  10305  subfzo0  10309  ceiqle  10384  modqval  10395  modqvalr  10396  flqpmodeq  10398  modq0  10400  mulqmod0  10401  negqmod0  10402  modqge0  10403  modqlt  10404  modqelico  10405  modqdiffl  10406  modqmulnn  10413  modqvalp1  10414  modqmuladdnn0  10439  qnegmod  10440  addmodid  10443  q2submod  10456  modifeq2int  10457  modfzo0difsn  10466  addmodlteq  10469  mulsubdivbinom2ap  10782  omgadd  10873  hashun  10876  redivap  11018  imdivap  11025  xrmaxltsup  11401  xrmaxadd  11404  xrlemininf  11414  xrminltinf  11415  climuni  11436  mulcn2  11455  fsumsplitsnun  11562  prodfap0  11688  fprodabs  11759  efsub  11824  cos12dec  11911  dvdsmodexp  11938  summodnegmod  11965  divalglemex  12063  divalg  12065  modremain  12070  ndvdssub  12071  fldivndvdslt  12076  nndvdslegcd  12102  dfgcd2  12151  mulgcd  12153  mulgcdr  12155  gcddiv  12156  rplpwr  12164  rppwr  12165  qredeq  12234  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  pw2dvdslemn  12303  hashgcdlem  12376  modprm0  12392  modprmn0modprm0  12394  pythagtriplem1  12403  pythagtriplem3  12405  pythagtriplem10  12407  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem11  12412  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem14  12415  pythagtriplem19  12420  pythagtrip  12421  dvdsprmpweqnn  12474  difsqpwdvds  12476  pcfaclem  12487  pcbc  12489  unennn  12554  ptex  12875  imasaddvallemg  12898  fvprif  12926  mgmsscl  12944  insubm  13057  mulginvcom  13217  mulgassr  13230  mulgmodid  13231  quselbasg  13300  ghmnsgima  13338  ringrng  13532  rmodislmodlem  13846  rmodislmod  13847  lssincl  13881  sralmod  13946  rnglidlmmgm  13992  rnglidlmsgrp  13993  rnglidlrng  13994  2idlcpblrng  14019  psrbaglesuppg  14158  ntrin  14292  elnei  14320  restco  14342  cnpnei  14387  cncnp2m  14399  sslm  14415  upxp  14440  blres  14602  metcnp3  14679  tgqioo  14715  ptolemy  14959  cxpcom  15071  logbgcd1irr  15099  logbprmirr  15104  lgslem1  15116  lgsneg  15140  lgsdilem  15143  lgsdir  15151  lgssq2  15157  lgsdirnn0  15163  gausslemma2dlem1a  15174