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  2826  vtoclgft  2851  vtoclegft  2875  ifbothdc  3637  ifnebibdc  3648  frirrg  4440  elirr  4632  en2lp  4645  reg3exmidlemwe  4670  sotri3  5126  funtpg  5371  fnprg  5375  fntpg  5376  funimaexglem  5403  fnco  5430  fvun1  5699  oprssov  6146  caovimo  6198  rdgivallem  6525  fnsnsplitdc  6649  funresdfunsndc  6650  f1dom2g  6905  mapxpen  7005  ssfidc  7095  sbthlemi4  7123  ordiso2  7198  updjud  7245  difinfsn  7263  mkvprop  7321  endjudisj  7388  distrnqg  7570  distrnq0  7642  prarloclem5  7683  cauappcvgprlemlol  7830  cauappcvgprlemupu  7832  caucvgprlemlol  7853  caucvgprlemupu  7855  caucvgprprlemlol  7881  caucvgprprlemupu  7883  cnegexlem2  8318  apcotr  8750  apadd1  8751  mulext1  8755  div2negap  8878  ltdiv2  9030  nndivtr  9148  difgtsumgt  9512  zdivmul  9533  gtndiv  9538  fzind  9558  eluzuzle  9726  eluzp1p1  9744  peano2uz  9774  qdivcl  9834  irrmul  9838  ledivge1le  9918  xrre2  10013  xaddass  10061  xltadd1  10068  xlt2add  10072  ubioc1  10121  ubicc2  10177  zltaddlt1le  10199  uzsubsubfz  10239  elfz1b  10282  fzp1nel  10296  fz0fzdiffz0  10322  difelfzle  10326  elfzo0  10378  elfzonlteqm1  10411  fzonn0p1p1  10414  fzosplitprm1  10435  fzoshftral  10439  subfzo0  10443  ceiqle  10530  modqval  10541  modqvalr  10542  flqpmodeq  10544  modq0  10546  mulqmod0  10547  negqmod0  10548  modqge0  10549  modqlt  10550  modqelico  10551  modqdiffl  10552  modqmulnn  10559  modqvalp1  10560  modqmuladdnn0  10585  qnegmod  10586  addmodid  10589  q2submod  10602  modifeq2int  10603  modfzo0difsn  10612  addmodlteq  10615  mulsubdivbinom2ap  10928  omgadd  11019  hashun  11022  ccatass  11138  lswccatn0lsw  11141  ccats1val2  11166  swrd00g  11176  swrdval2  11178  swrdlen  11179  swrdfv  11180  swrdfv0  11181  swrdnd  11186  swrdlen2  11189  swrdfv2  11190  swrdsbslen  11193  swrdspsleq  11194  ccatswrd  11197  pfxfv  11211  pfxn0  11215  pfxnd  11216  pfxsuff1eqwrdeq  11226  pfxpfx  11235  ccats1pfxeq  11241  ccatopth2  11244  wrd2ind  11250  pfxccatin12lem3  11259  pfxccat3  11261  swrdccat  11262  pfxccat3a  11265  redivap  11380  imdivap  11387  xrmaxltsup  11764  xrmaxadd  11767  xrlemininf  11777  xrminltinf  11778  climuni  11799  mulcn2  11818  fsumsplitsnun  11925  prodfap0  12051  fprodabs  12122  efsub  12187  cos12dec  12274  dvdsmodexp  12301  summodnegmod  12328  divalglemex  12428  divalg  12430  modremain  12435  ndvdssub  12436  fldivndvdslt  12443  bitsfzo  12461  nndvdslegcd  12481  dfgcd2  12530  mulgcd  12532  mulgcdr  12534  gcddiv  12535  rplpwr  12543  rppwr  12544  qredeq  12613  divgcdcoprmex  12619  cncongr1  12620  cncongr2  12621  pw2dvdslemn  12682  hashgcdlem  12755  modprm0  12772  modprmn0modprm0  12774  pythagtriplem1  12783  pythagtriplem3  12785  pythagtriplem10  12787  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem11  12792  pythagtriplem12  12793  pythagtriplem13  12794  pythagtriplem14  12795  pythagtriplem19  12800  pythagtrip  12801  dvdsprmpweqnn  12854  difsqpwdvds  12856  pcfaclem  12867  pcbc  12869  unennn  12963  ptex  13292  imasaddvallemg  13343  fvprif  13371  mgmsscl  13389  insubm  13513  mulginvcom  13679  mulgassr  13692  mulgmodid  13693  quselbasg  13762  ghmnsgima  13800  ringrng  13994  rmodislmodlem  14308  rmodislmod  14309  lssincl  14343  sralmod  14408  rnglidlmmgm  14454  rnglidlmsgrp  14455  rnglidlrng  14456  2idlcpblrng  14481  psrbaglesuppg  14630  ntrin  14792  elnei  14820  restco  14842  cnpnei  14887  cncnp2m  14899  sslm  14915  upxp  14940  blres  15102  metcnp3  15179  tgqioo  15223  dvply1  15433  ptolemy  15492  cxpcom  15606  logbgcd1irr  15635  logbprmirr  15640  lgslem1  15673  lgsneg  15697  lgsdilem  15700  lgsdir  15708  lgssq2  15714  lgsdirnn0  15720  gausslemma2dlem1a  15731  2lgslem1a1  15759  incistruhgr  15884  upgrex  15897  uhgr2edg  15998