Theorem 3ad2ant2 1046

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simp2l  1050  simp2r  1051  simp21  1057  simp22  1058  simp23  1059  simp2ll  1091  simp2lr  1092  simp2rl  1093  simp2rr  1094  simp2l1  1123  simp2l2  1124  simp2l3  1125  simp2r1  1126  simp2r2  1127  simp2r3  1128  simp21l  1141  simp21r  1142  simp22l  1143  simp22r  1144  simp23l  1145  simp23r  1146  simp211  1162  simp212  1163  simp213  1164  simp221  1165  simp222  1166  simp223  1167  simp231  1168  simp232  1169  simp233  1170  3anim123i  1211  3jaao  1345  ceqsalt  2840  vtoclgft  2865  vtoclegft  2889  ifbothdc  3657  ifnebibdc  3668  frirrg  4471  elirr  4663  en2lp  4676  reg3exmidlemwe  4701  sotri3  5161  funtpg  5407  fnprg  5411  fntpg  5412  funimaexglem  5439  fnco  5466  fresaunres2disj  5545  fvun1  5743  oprssov  6196  caovimo  6248  suppsnopdc  6450  funsssuppss  6458  rdgivallem  6612  fnsnsplitdc  6738  funresdfunsndc  6739  mapsnd  6923  f1dom2g  6995  mapxpen  7101  ssfidc  7198  sbthlemi4  7230  ordiso2  7326  updjud  7373  difinfsn  7391  mkvprop  7449  endjudisj  7517  distrnqg  7702  distrnq0  7774  prarloclem5  7815  cauappcvgprlemlol  7962  cauappcvgprlemupu  7964  caucvgprlemlol  7985  caucvgprlemupu  7987  caucvgprprlemlol  8013  caucvgprprlemupu  8015  cnegexlem2  8449  apcotr  8881  apadd1  8882  mulext1  8886  div2negap  9009  ltdiv2  9161  nndivtr  9279  difgtsumgt  9647  zdivmul  9668  gtndiv  9673  fzind  9693  eluzuzle  9862  eluzp1p1  9880  peano2uz  9915  qdivcl  9975  irrmul  9979  ledivge1le  10059  xrre2  10154  xaddass  10202  xltadd1  10209  xlt2add  10213  ubioc1  10262  ubicc2  10318  zltaddlt1le  10341  uzsubsubfz  10381  elfz1b  10424  fzp1nel  10438  fz0fzdiffz0  10464  difelfzle  10468  elfzo0  10520  elfzonlteqm1  10555  fzonn0p1p1  10558  fzosplitprm1  10580  fzoshftral  10584  subfzo0  10588  ceiqle  10675  modqval  10686  modqvalr  10687  flqpmodeq  10689  modq0  10691  mulqmod0  10692  negqmod0  10693  modqge0  10694  modqlt  10695  modqelico  10696  modqdiffl  10697  modqmulnn  10704  modqvalp1  10705  modqmuladdnn0  10730  qnegmod  10731  addmodid  10734  q2submod  10747  modifeq2int  10748  modfzo0difsn  10757  addmodlteq  10760  mulsubdivbinom2ap  11073  omgadd  11166  hashun  11169  ccatass  11296  lswccatn0lsw  11299  ccats1val2  11328  swrd00g  11341  swrdval2  11343  swrdlen  11344  swrdfv  11345  swrdfv0  11346  swrdnd  11351  swrdlen2  11354  swrdfv2  11355  swrdsbslen  11358  swrdspsleq  11359  ccatswrd  11362  pfxfv  11376  pfxn0  11380  pfxnd  11381  pfxsuff1eqwrdeq  11391  pfxpfx  11400  ccats1pfxeq  11406  ccatopth2  11409  wrd2ind  11415  pfxccatin12lem3  11424  pfxccat3  11426  swrdccat  11427  pfxccat3a  11430  redivap  11559  imdivap  11566  xrmaxltsup  11943  xrmaxadd  11946  xrlemininf  11956  xrminltinf  11957  climuni  11978  mulcn2  11997  fsumsplitsnun  12105  prodfap0  12231  fprodabs  12302  efsub  12367  cos12dec  12454  dvdsmodexp  12481  summodnegmod  12508  divalglemex  12608  divalg  12610  modremain  12615  ndvdssub  12616  fldivndvdslt  12623  bitsfzo  12641  nndvdslegcd  12661  dfgcd2  12710  mulgcd  12712  mulgcdr  12714  gcddiv  12715  rplpwr  12723  rppwr  12724  qredeq  12793  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  pw2dvdslemn  12862  hashgcdlem  12935  modprm0  12952  modprmn0modprm0  12954  pythagtriplem1  12963  pythagtriplem3  12965  pythagtriplem10  12967  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem11  12972  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem14  12975  pythagtriplem19  12980  pythagtrip  12981  dvdsprmpweqnn  13034  difsqpwdvds  13036  pcfaclem  13047  pcbc  13049  unennn  13148  ptex  13477  imasaddvallemg  13528  fvprif  13556  mgmsscl  13574  insubm  13698  mulginvcom  13864  mulgassr  13877  mulgmodid  13878  quselbasg  13947  ghmnsgima  13985  ringrng  14180  rmodislmodlem  14498  rmodislmod  14499  lssincl  14533  sralmod  14598  rnglidlmmgm  14644  rnglidlmsgrp  14645  rnglidlrng  14646  2idlcpblrng  14671  psrbaglesuppg  14821  psrbagaddclfi  14825  ntrin  14989  elnei  15017  restco  15039  cnpnei  15084  cncnp2m  15096  sslm  15112  upxp  15137  blres  15299  metcnp3  15376  tgqioo  15420  dvply1  15630  ptolemy  15689  cxpcom  15803  logbgcd1irr  15832  logbprmirr  15837  pellexlem1  15845  lgslem1  15873  lgsneg  15897  lgsdilem  15900  lgsdir  15908  lgssq2  15914  lgsdirnn0  15920  gausslemma2dlem1a  15931  2lgslem1a1  15959  incistruhgr  16085  upgrex  16098  uhgr2edg  16201  usgr2v1e2w  16241  issubgr2  16253  0uhgrsubgr  16260  subgrfun  16262  subgreldmiedg  16264  subumgredg2en  16266  iedginwlk  16352  uspgr2wlkeq2  16361  umgrclwwlkge2  16397  clwwlkext2edg  16417  clwwlknccat  16418  umgr2cwwk2dif  16419  umgr2cwwkdifex  16420  clwwlknonex2  16434  gfsumsn  16867