Theorem 3ad2ant2 1043

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  simp2l  1047  simp2r  1048  simp21  1054  simp22  1055  simp23  1056  simp2ll  1088  simp2lr  1089  simp2rl  1090  simp2rr  1091  simp2l1  1120  simp2l2  1121  simp2l3  1122  simp2r1  1123  simp2r2  1124  simp2r3  1125  simp21l  1138  simp21r  1139  simp22l  1140  simp22r  1141  simp23l  1142  simp23r  1143  simp211  1159  simp212  1160  simp213  1161  simp221  1162  simp222  1163  simp223  1164  simp231  1165  simp232  1166  simp233  1167  3anim123i  1208  3jaao  1342  ceqsalt  2827  vtoclgft  2852  vtoclegft  2876  ifbothdc  3638  ifnebibdc  3649  frirrg  4445  elirr  4637  en2lp  4650  reg3exmidlemwe  4675  sotri3  5133  funtpg  5378  fnprg  5382  fntpg  5383  funimaexglem  5410  fnco  5437  fvun1  5708  oprssov  6159  caovimo  6211  rdgivallem  6542  fnsnsplitdc  6668  funresdfunsndc  6669  f1dom2g  6924  mapxpen  7029  ssfidc  7122  sbthlemi4  7150  ordiso2  7225  updjud  7272  difinfsn  7290  mkvprop  7348  endjudisj  7415  distrnqg  7597  distrnq0  7669  prarloclem5  7710  cauappcvgprlemlol  7857  cauappcvgprlemupu  7859  caucvgprlemlol  7880  caucvgprlemupu  7882  caucvgprprlemlol  7908  caucvgprprlemupu  7910  cnegexlem2  8345  apcotr  8777  apadd1  8778  mulext1  8782  div2negap  8905  ltdiv2  9057  nndivtr  9175  difgtsumgt  9539  zdivmul  9560  gtndiv  9565  fzind  9585  eluzuzle  9754  eluzp1p1  9772  peano2uz  9807  qdivcl  9867  irrmul  9871  ledivge1le  9951  xrre2  10046  xaddass  10094  xltadd1  10101  xlt2add  10105  ubioc1  10154  ubicc2  10210  zltaddlt1le  10232  uzsubsubfz  10272  elfz1b  10315  fzp1nel  10329  fz0fzdiffz0  10355  difelfzle  10359  elfzo0  10411  elfzonlteqm1  10445  fzonn0p1p1  10448  fzosplitprm1  10470  fzoshftral  10474  subfzo0  10478  ceiqle  10565  modqval  10576  modqvalr  10577  flqpmodeq  10579  modq0  10581  mulqmod0  10582  negqmod0  10583  modqge0  10584  modqlt  10585  modqelico  10586  modqdiffl  10587  modqmulnn  10594  modqvalp1  10595  modqmuladdnn0  10620  qnegmod  10621  addmodid  10624  q2submod  10637  modifeq2int  10638  modfzo0difsn  10647  addmodlteq  10650  mulsubdivbinom2ap  10963  omgadd  11055  hashun  11058  ccatass  11175  lswccatn0lsw  11178  ccats1val2  11207  swrd00g  11220  swrdval2  11222  swrdlen  11223  swrdfv  11224  swrdfv0  11225  swrdnd  11230  swrdlen2  11233  swrdfv2  11234  swrdsbslen  11237  swrdspsleq  11238  ccatswrd  11241  pfxfv  11255  pfxn0  11259  pfxnd  11260  pfxsuff1eqwrdeq  11270  pfxpfx  11279  ccats1pfxeq  11285  ccatopth2  11288  wrd2ind  11294  pfxccatin12lem3  11303  pfxccat3  11305  swrdccat  11306  pfxccat3a  11309  redivap  11425  imdivap  11432  xrmaxltsup  11809  xrmaxadd  11812  xrlemininf  11822  xrminltinf  11823  climuni  11844  mulcn2  11863  fsumsplitsnun  11970  prodfap0  12096  fprodabs  12167  efsub  12232  cos12dec  12319  dvdsmodexp  12346  summodnegmod  12373  divalglemex  12473  divalg  12475  modremain  12480  ndvdssub  12481  fldivndvdslt  12488  bitsfzo  12506  nndvdslegcd  12526  dfgcd2  12575  mulgcd  12577  mulgcdr  12579  gcddiv  12580  rplpwr  12588  rppwr  12589  qredeq  12658  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  pw2dvdslemn  12727  hashgcdlem  12800  modprm0  12817  modprmn0modprm0  12819  pythagtriplem1  12828  pythagtriplem3  12830  pythagtriplem10  12832  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem11  12837  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem14  12840  pythagtriplem19  12845  pythagtrip  12846  dvdsprmpweqnn  12899  difsqpwdvds  12901  pcfaclem  12912  pcbc  12914  unennn  13008  ptex  13337  imasaddvallemg  13388  fvprif  13416  mgmsscl  13434  insubm  13558  mulginvcom  13724  mulgassr  13737  mulgmodid  13738  quselbasg  13807  ghmnsgima  13845  ringrng  14039  rmodislmodlem  14354  rmodislmod  14355  lssincl  14389  sralmod  14454  rnglidlmmgm  14500  rnglidlmsgrp  14501  rnglidlrng  14502  2idlcpblrng  14527  psrbaglesuppg  14676  ntrin  14838  elnei  14866  restco  14888  cnpnei  14933  cncnp2m  14945  sslm  14961  upxp  14986  blres  15148  metcnp3  15225  tgqioo  15269  dvply1  15479  ptolemy  15538  cxpcom  15652  logbgcd1irr  15681  logbprmirr  15686  lgslem1  15719  lgsneg  15743  lgsdilem  15746  lgsdir  15754  lgssq2  15760  lgsdirnn0  15766  gausslemma2dlem1a  15777  2lgslem1a1  15805  incistruhgr  15931  upgrex  15944  uhgr2edg  16045  usgr2v1e2w  16085  iedginwlk  16154  uspgr2wlkeq2  16163  umgrclwwlkge2  16197  clwwlkext2edg  16217  clwwlknccat  16218  umgr2cwwk2dif  16219  umgr2cwwkdifex  16220  clwwlknonex2  16234