Theorem 3ad2ant2 1021

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp2l  1025  simp2r  1026  simp21  1032  simp22  1033  simp23  1034  simp2ll  1066  simp2lr  1067  simp2rl  1068  simp2rr  1069  simp2l1  1098  simp2l2  1099  simp2l3  1100  simp2r1  1101  simp2r2  1102  simp2r3  1103  simp21l  1116  simp21r  1117  simp22l  1118  simp22r  1119  simp23l  1120  simp23r  1121  simp211  1137  simp212  1138  simp213  1139  simp221  1140  simp222  1141  simp223  1142  simp231  1143  simp232  1144  simp233  1145  3anim123i  1186  3jaao  1320  ceqsalt  2797  vtoclgft  2822  vtoclegft  2844  ifbothdc  3604  ifnebibdc  3614  frirrg  4396  elirr  4588  en2lp  4601  reg3exmidlemwe  4626  sotri3  5080  funtpg  5324  fnprg  5328  fntpg  5329  funimaexglem  5356  fnco  5383  fvun1  5644  oprssov  6087  caovimo  6139  rdgivallem  6466  fnsnsplitdc  6590  funresdfunsndc  6591  f1dom2g  6846  mapxpen  6944  ssfidc  7033  sbthlemi4  7061  ordiso2  7136  updjud  7183  difinfsn  7201  mkvprop  7259  endjudisj  7321  distrnqg  7499  distrnq0  7571  prarloclem5  7612  cauappcvgprlemlol  7759  cauappcvgprlemupu  7761  caucvgprlemlol  7782  caucvgprlemupu  7784  caucvgprprlemlol  7810  caucvgprprlemupu  7812  cnegexlem2  8247  apcotr  8679  apadd1  8680  mulext1  8684  div2negap  8807  ltdiv2  8959  nndivtr  9077  difgtsumgt  9441  zdivmul  9462  gtndiv  9467  fzind  9487  eluzuzle  9655  eluzp1p1  9673  peano2uz  9703  qdivcl  9763  irrmul  9767  ledivge1le  9847  xrre2  9942  xaddass  9990  xltadd1  9997  xlt2add  10001  ubioc1  10050  ubicc2  10106  zltaddlt1le  10128  uzsubsubfz  10168  elfz1b  10211  fzp1nel  10225  fz0fzdiffz0  10251  difelfzle  10255  elfzo0  10304  elfzonlteqm1  10337  fzonn0p1p1  10340  fzosplitprm1  10361  fzoshftral  10365  subfzo0  10369  ceiqle  10456  modqval  10467  modqvalr  10468  flqpmodeq  10470  modq0  10472  mulqmod0  10473  negqmod0  10474  modqge0  10475  modqlt  10476  modqelico  10477  modqdiffl  10478  modqmulnn  10485  modqvalp1  10486  modqmuladdnn0  10511  qnegmod  10512  addmodid  10515  q2submod  10528  modifeq2int  10529  modfzo0difsn  10538  addmodlteq  10541  mulsubdivbinom2ap  10854  omgadd  10945  hashun  10948  ccatass  11062  lswccatn0lsw  11065  redivap  11127  imdivap  11134  xrmaxltsup  11511  xrmaxadd  11514  xrlemininf  11524  xrminltinf  11525  climuni  11546  mulcn2  11565  fsumsplitsnun  11672  prodfap0  11798  fprodabs  11869  efsub  11934  cos12dec  12021  dvdsmodexp  12048  summodnegmod  12075  divalglemex  12175  divalg  12177  modremain  12182  ndvdssub  12183  fldivndvdslt  12190  bitsfzo  12208  nndvdslegcd  12228  dfgcd2  12277  mulgcd  12279  mulgcdr  12281  gcddiv  12282  rplpwr  12290  rppwr  12291  qredeq  12360  divgcdcoprmex  12366  cncongr1  12367  cncongr2  12368  pw2dvdslemn  12429  hashgcdlem  12502  modprm0  12519  modprmn0modprm0  12521  pythagtriplem1  12530  pythagtriplem3  12532  pythagtriplem10  12534  pythagtriplem6  12535  pythagtriplem7  12536  pythagtriplem11  12539  pythagtriplem12  12540  pythagtriplem13  12541  pythagtriplem14  12542  pythagtriplem19  12547  pythagtrip  12548  dvdsprmpweqnn  12601  difsqpwdvds  12603  pcfaclem  12614  pcbc  12616  unennn  12710  ptex  13038  imasaddvallemg  13089  fvprif  13117  mgmsscl  13135  insubm  13259  mulginvcom  13425  mulgassr  13438  mulgmodid  13439  quselbasg  13508  ghmnsgima  13546  ringrng  13740  rmodislmodlem  14054  rmodislmod  14055  lssincl  14089  sralmod  14154  rnglidlmmgm  14200  rnglidlmsgrp  14201  rnglidlrng  14202  2idlcpblrng  14227  psrbaglesuppg  14376  ntrin  14538  elnei  14566  restco  14588  cnpnei  14633  cncnp2m  14645  sslm  14661  upxp  14686  blres  14848  metcnp3  14925  tgqioo  14969  dvply1  15179  ptolemy  15238  cxpcom  15352  logbgcd1irr  15381  logbprmirr  15386  lgslem1  15419  lgsneg  15443  lgsdilem  15446  lgsdir  15454  lgssq2  15460  lgsdirnn0  15466  gausslemma2dlem1a  15477  2lgslem1a1  15505