Theorem 3ad2ant2 1045

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simp2l  1049  simp2r  1050  simp21  1056  simp22  1057  simp23  1058  simp2ll  1090  simp2lr  1091  simp2rl  1092  simp2rr  1093  simp2l1  1122  simp2l2  1123  simp2l3  1124  simp2r1  1125  simp2r2  1126  simp2r3  1127  simp21l  1140  simp21r  1141  simp22l  1142  simp22r  1143  simp23l  1144  simp23r  1145  simp211  1161  simp212  1162  simp213  1163  simp221  1164  simp222  1165  simp223  1166  simp231  1167  simp232  1168  simp233  1169  3anim123i  1210  3jaao  1344  ceqsalt  2829  vtoclgft  2854  vtoclegft  2878  ifbothdc  3640  ifnebibdc  3651  frirrg  4447  elirr  4639  en2lp  4652  reg3exmidlemwe  4677  sotri3  5135  funtpg  5381  fnprg  5385  fntpg  5386  funimaexglem  5413  fnco  5440  fvun1  5712  oprssov  6163  caovimo  6215  rdgivallem  6546  fnsnsplitdc  6672  funresdfunsndc  6673  f1dom2g  6928  mapxpen  7033  ssfidc  7129  sbthlemi4  7158  ordiso2  7233  updjud  7280  difinfsn  7298  mkvprop  7356  endjudisj  7424  distrnqg  7606  distrnq0  7678  prarloclem5  7719  cauappcvgprlemlol  7866  cauappcvgprlemupu  7868  caucvgprlemlol  7889  caucvgprlemupu  7891  caucvgprprlemlol  7917  caucvgprprlemupu  7919  cnegexlem2  8354  apcotr  8786  apadd1  8787  mulext1  8791  div2negap  8914  ltdiv2  9066  nndivtr  9184  difgtsumgt  9548  zdivmul  9569  gtndiv  9574  fzind  9594  eluzuzle  9763  eluzp1p1  9781  peano2uz  9816  qdivcl  9876  irrmul  9880  ledivge1le  9960  xrre2  10055  xaddass  10103  xltadd1  10110  xlt2add  10114  ubioc1  10163  ubicc2  10219  zltaddlt1le  10241  uzsubsubfz  10281  elfz1b  10324  fzp1nel  10338  fz0fzdiffz0  10364  difelfzle  10368  elfzo0  10420  elfzonlteqm1  10454  fzonn0p1p1  10457  fzosplitprm1  10479  fzoshftral  10483  subfzo0  10487  ceiqle  10574  modqval  10585  modqvalr  10586  flqpmodeq  10588  modq0  10590  mulqmod0  10591  negqmod0  10592  modqge0  10593  modqlt  10594  modqelico  10595  modqdiffl  10596  modqmulnn  10603  modqvalp1  10604  modqmuladdnn0  10629  qnegmod  10630  addmodid  10633  q2submod  10646  modifeq2int  10647  modfzo0difsn  10656  addmodlteq  10659  mulsubdivbinom2ap  10972  omgadd  11064  hashun  11067  ccatass  11184  lswccatn0lsw  11187  ccats1val2  11216  swrd00g  11229  swrdval2  11231  swrdlen  11232  swrdfv  11233  swrdfv0  11234  swrdnd  11239  swrdlen2  11242  swrdfv2  11243  swrdsbslen  11246  swrdspsleq  11247  ccatswrd  11250  pfxfv  11264  pfxn0  11268  pfxnd  11269  pfxsuff1eqwrdeq  11279  pfxpfx  11288  ccats1pfxeq  11294  ccatopth2  11297  wrd2ind  11303  pfxccatin12lem3  11312  pfxccat3  11314  swrdccat  11315  pfxccat3a  11318  redivap  11434  imdivap  11441  xrmaxltsup  11818  xrmaxadd  11821  xrlemininf  11831  xrminltinf  11832  climuni  11853  mulcn2  11872  fsumsplitsnun  11979  prodfap0  12105  fprodabs  12176  efsub  12241  cos12dec  12328  dvdsmodexp  12355  summodnegmod  12382  divalglemex  12482  divalg  12484  modremain  12489  ndvdssub  12490  fldivndvdslt  12497  bitsfzo  12515  nndvdslegcd  12535  dfgcd2  12584  mulgcd  12586  mulgcdr  12588  gcddiv  12589  rplpwr  12597  rppwr  12598  qredeq  12667  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  pw2dvdslemn  12736  hashgcdlem  12809  modprm0  12826  modprmn0modprm0  12828  pythagtriplem1  12837  pythagtriplem3  12839  pythagtriplem10  12841  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem11  12846  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem14  12849  pythagtriplem19  12854  pythagtrip  12855  dvdsprmpweqnn  12908  difsqpwdvds  12910  pcfaclem  12921  pcbc  12923  unennn  13017  ptex  13346  imasaddvallemg  13397  fvprif  13425  mgmsscl  13443  insubm  13567  mulginvcom  13733  mulgassr  13746  mulgmodid  13747  quselbasg  13816  ghmnsgima  13854  ringrng  14048  rmodislmodlem  14363  rmodislmod  14364  lssincl  14398  sralmod  14463  rnglidlmmgm  14509  rnglidlmsgrp  14510  rnglidlrng  14511  2idlcpblrng  14536  psrbaglesuppg  14685  ntrin  14847  elnei  14875  restco  14897  cnpnei  14942  cncnp2m  14954  sslm  14970  upxp  14995  blres  15157  metcnp3  15234  tgqioo  15278  dvply1  15488  ptolemy  15547  cxpcom  15661  logbgcd1irr  15690  logbprmirr  15695  lgslem1  15728  lgsneg  15752  lgsdilem  15755  lgsdir  15763  lgssq2  15769  lgsdirnn0  15775  gausslemma2dlem1a  15786  2lgslem1a1  15814  incistruhgr  15940  upgrex  15953  uhgr2edg  16056  usgr2v1e2w  16096  issubgr2  16108  0uhgrsubgr  16115  subgrfun  16117  subgreldmiedg  16119  subumgredg2en  16121  iedginwlk  16207  uspgr2wlkeq2  16216  umgrclwwlkge2  16252  clwwlkext2edg  16272  clwwlknccat  16273  umgr2cwwk2dif  16274  umgr2cwwkdifex  16275  clwwlknonex2  16289