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  6164  caovimo  6216  rdgivallem  6547  fnsnsplitdc  6673  funresdfunsndc  6674  f1dom2g  6929  mapxpen  7034  ssfidc  7130  sbthlemi4  7159  ordiso2  7234  updjud  7281  difinfsn  7299  mkvprop  7357  endjudisj  7425  distrnqg  7607  distrnq0  7679  prarloclem5  7720  cauappcvgprlemlol  7867  cauappcvgprlemupu  7869  caucvgprlemlol  7890  caucvgprlemupu  7892  caucvgprprlemlol  7918  caucvgprprlemupu  7920  cnegexlem2  8355  apcotr  8787  apadd1  8788  mulext1  8792  div2negap  8915  ltdiv2  9067  nndivtr  9185  difgtsumgt  9549  zdivmul  9570  gtndiv  9575  fzind  9595  eluzuzle  9764  eluzp1p1  9782  peano2uz  9817  qdivcl  9877  irrmul  9881  ledivge1le  9961  xrre2  10056  xaddass  10104  xltadd1  10111  xlt2add  10115  ubioc1  10164  ubicc2  10220  zltaddlt1le  10242  uzsubsubfz  10282  elfz1b  10325  fzp1nel  10339  fz0fzdiffz0  10365  difelfzle  10369  elfzo0  10421  elfzonlteqm1  10456  fzonn0p1p1  10459  fzosplitprm1  10481  fzoshftral  10485  subfzo0  10489  ceiqle  10576  modqval  10587  modqvalr  10588  flqpmodeq  10590  modq0  10592  mulqmod0  10593  negqmod0  10594  modqge0  10595  modqlt  10596  modqelico  10597  modqdiffl  10598  modqmulnn  10605  modqvalp1  10606  modqmuladdnn0  10631  qnegmod  10632  addmodid  10635  q2submod  10648  modifeq2int  10649  modfzo0difsn  10658  addmodlteq  10661  mulsubdivbinom2ap  10974  omgadd  11066  hashun  11069  ccatass  11189  lswccatn0lsw  11192  ccats1val2  11221  swrd00g  11234  swrdval2  11236  swrdlen  11237  swrdfv  11238  swrdfv0  11239  swrdnd  11244  swrdlen2  11247  swrdfv2  11248  swrdsbslen  11251  swrdspsleq  11252  ccatswrd  11255  pfxfv  11269  pfxn0  11273  pfxnd  11274  pfxsuff1eqwrdeq  11284  pfxpfx  11293  ccats1pfxeq  11299  ccatopth2  11302  wrd2ind  11308  pfxccatin12lem3  11317  pfxccat3  11319  swrdccat  11320  pfxccat3a  11323  redivap  11439  imdivap  11446  xrmaxltsup  11823  xrmaxadd  11826  xrlemininf  11836  xrminltinf  11837  climuni  11858  mulcn2  11877  fsumsplitsnun  11985  prodfap0  12111  fprodabs  12182  efsub  12247  cos12dec  12334  dvdsmodexp  12361  summodnegmod  12388  divalglemex  12488  divalg  12490  modremain  12495  ndvdssub  12496  fldivndvdslt  12503  bitsfzo  12521  nndvdslegcd  12541  dfgcd2  12590  mulgcd  12592  mulgcdr  12594  gcddiv  12595  rplpwr  12603  rppwr  12604  qredeq  12673  divgcdcoprmex  12679  cncongr1  12680  cncongr2  12681  pw2dvdslemn  12742  hashgcdlem  12815  modprm0  12832  modprmn0modprm0  12834  pythagtriplem1  12843  pythagtriplem3  12845  pythagtriplem10  12847  pythagtriplem6  12848  pythagtriplem7  12849  pythagtriplem11  12852  pythagtriplem12  12853  pythagtriplem13  12854  pythagtriplem14  12855  pythagtriplem19  12860  pythagtrip  12861  dvdsprmpweqnn  12914  difsqpwdvds  12916  pcfaclem  12927  pcbc  12929  unennn  13023  ptex  13352  imasaddvallemg  13403  fvprif  13431  mgmsscl  13449  insubm  13573  mulginvcom  13739  mulgassr  13752  mulgmodid  13753  quselbasg  13822  ghmnsgima  13860  ringrng  14055  rmodislmodlem  14370  rmodislmod  14371  lssincl  14405  sralmod  14470  rnglidlmmgm  14516  rnglidlmsgrp  14517  rnglidlrng  14518  2idlcpblrng  14543  psrbaglesuppg  14692  ntrin  14854  elnei  14882  restco  14904  cnpnei  14949  cncnp2m  14961  sslm  14977  upxp  15002  blres  15164  metcnp3  15241  tgqioo  15285  dvply1  15495  ptolemy  15554  cxpcom  15668  logbgcd1irr  15697  logbprmirr  15702  lgslem1  15735  lgsneg  15759  lgsdilem  15762  lgsdir  15770  lgssq2  15776  lgsdirnn0  15782  gausslemma2dlem1a  15793  2lgslem1a1  15821  incistruhgr  15947  upgrex  15960  uhgr2edg  16063  usgr2v1e2w  16103  issubgr2  16115  0uhgrsubgr  16122  subgrfun  16124  subgreldmiedg  16126  subumgredg2en  16128  iedginwlk  16214  uspgr2wlkeq2  16223  umgrclwwlkge2  16259  clwwlkext2edg  16279  clwwlknccat  16280  umgr2cwwk2dif  16281  umgr2cwwkdifex  16282  clwwlknonex2  16296  gfsumsn  16712