Theorem 3ad2ant2 1046

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simp2l  1050  simp2r  1051  simp21  1057  simp22  1058  simp23  1059  simp2ll  1091  simp2lr  1092  simp2rl  1093  simp2rr  1094  simp2l1  1123  simp2l2  1124  simp2l3  1125  simp2r1  1126  simp2r2  1127  simp2r3  1128  simp21l  1141  simp21r  1142  simp22l  1143  simp22r  1144  simp23l  1145  simp23r  1146  simp211  1162  simp212  1163  simp213  1164  simp221  1165  simp222  1166  simp223  1167  simp231  1168  simp232  1169  simp233  1170  3anim123i  1211  3jaao  1345  ceqsalt  2830  vtoclgft  2855  vtoclegft  2879  ifbothdc  3644  ifnebibdc  3655  frirrg  4453  elirr  4645  en2lp  4658  reg3exmidlemwe  4683  sotri3  5142  funtpg  5388  fnprg  5392  fntpg  5393  funimaexglem  5420  fnco  5447  fvun1  5721  oprssov  6174  caovimo  6226  suppsnopdc  6428  funsssuppss  6436  rdgivallem  6590  fnsnsplitdc  6716  funresdfunsndc  6717  f1dom2g  6972  mapxpen  7077  ssfidc  7173  sbthlemi4  7202  ordiso2  7277  updjud  7324  difinfsn  7342  mkvprop  7400  endjudisj  7468  distrnqg  7650  distrnq0  7722  prarloclem5  7763  cauappcvgprlemlol  7910  cauappcvgprlemupu  7912  caucvgprlemlol  7933  caucvgprlemupu  7935  caucvgprprlemlol  7961  caucvgprprlemupu  7963  cnegexlem2  8397  apcotr  8829  apadd1  8830  mulext1  8834  div2negap  8957  ltdiv2  9109  nndivtr  9227  difgtsumgt  9593  zdivmul  9614  gtndiv  9619  fzind  9639  eluzuzle  9808  eluzp1p1  9826  peano2uz  9861  qdivcl  9921  irrmul  9925  ledivge1le  10005  xrre2  10100  xaddass  10148  xltadd1  10155  xlt2add  10159  ubioc1  10208  ubicc2  10264  zltaddlt1le  10287  uzsubsubfz  10327  elfz1b  10370  fzp1nel  10384  fz0fzdiffz0  10410  difelfzle  10414  elfzo0  10466  elfzonlteqm1  10501  fzonn0p1p1  10504  fzosplitprm1  10526  fzoshftral  10530  subfzo0  10534  ceiqle  10621  modqval  10632  modqvalr  10633  flqpmodeq  10635  modq0  10637  mulqmod0  10638  negqmod0  10639  modqge0  10640  modqlt  10641  modqelico  10642  modqdiffl  10643  modqmulnn  10650  modqvalp1  10651  modqmuladdnn0  10676  qnegmod  10677  addmodid  10680  q2submod  10693  modifeq2int  10694  modfzo0difsn  10703  addmodlteq  10706  mulsubdivbinom2ap  11019  omgadd  11111  hashun  11114  ccatass  11234  lswccatn0lsw  11237  ccats1val2  11266  swrd00g  11279  swrdval2  11281  swrdlen  11282  swrdfv  11283  swrdfv0  11284  swrdnd  11289  swrdlen2  11292  swrdfv2  11293  swrdsbslen  11296  swrdspsleq  11297  ccatswrd  11300  pfxfv  11314  pfxn0  11318  pfxnd  11319  pfxsuff1eqwrdeq  11329  pfxpfx  11338  ccats1pfxeq  11344  ccatopth2  11347  wrd2ind  11353  pfxccatin12lem3  11362  pfxccat3  11364  swrdccat  11365  pfxccat3a  11368  redivap  11497  imdivap  11504  xrmaxltsup  11881  xrmaxadd  11884  xrlemininf  11894  xrminltinf  11895  climuni  11916  mulcn2  11935  fsumsplitsnun  12043  prodfap0  12169  fprodabs  12240  efsub  12305  cos12dec  12392  dvdsmodexp  12419  summodnegmod  12446  divalglemex  12546  divalg  12548  modremain  12553  ndvdssub  12554  fldivndvdslt  12561  bitsfzo  12579  nndvdslegcd  12599  dfgcd2  12648  mulgcd  12650  mulgcdr  12652  gcddiv  12653  rplpwr  12661  rppwr  12662  qredeq  12731  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  pw2dvdslemn  12800  hashgcdlem  12873  modprm0  12890  modprmn0modprm0  12892  pythagtriplem1  12901  pythagtriplem3  12903  pythagtriplem10  12905  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem11  12910  pythagtriplem12  12911  pythagtriplem13  12912  pythagtriplem14  12913  pythagtriplem19  12918  pythagtrip  12919  dvdsprmpweqnn  12972  difsqpwdvds  12974  pcfaclem  12985  pcbc  12987  unennn  13081  ptex  13410  imasaddvallemg  13461  fvprif  13489  mgmsscl  13507  insubm  13631  mulginvcom  13797  mulgassr  13810  mulgmodid  13811  quselbasg  13880  ghmnsgima  13918  ringrng  14113  rmodislmodlem  14429  rmodislmod  14430  lssincl  14464  sralmod  14529  rnglidlmmgm  14575  rnglidlmsgrp  14576  rnglidlrng  14577  2idlcpblrng  14602  psrbaglesuppg  14751  ntrin  14918  elnei  14946  restco  14968  cnpnei  15013  cncnp2m  15025  sslm  15041  upxp  15066  blres  15228  metcnp3  15305  tgqioo  15349  dvply1  15559  ptolemy  15618  cxpcom  15732  logbgcd1irr  15761  logbprmirr  15766  pellexlem1  15774  lgslem1  15802  lgsneg  15826  lgsdilem  15829  lgsdir  15837  lgssq2  15843  lgsdirnn0  15849  gausslemma2dlem1a  15860  2lgslem1a1  15888  incistruhgr  16014  upgrex  16027  uhgr2edg  16130  usgr2v1e2w  16170  issubgr2  16182  0uhgrsubgr  16189  subgrfun  16191  subgreldmiedg  16193  subumgredg2en  16195  iedginwlk  16281  uspgr2wlkeq2  16290  umgrclwwlkge2  16326  clwwlkext2edg  16346  clwwlknccat  16347  umgr2cwwk2dif  16348  umgr2cwwkdifex  16349  clwwlknonex2  16363  gfsumsn  16797