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  4441  elirr  4633  en2lp  4646  reg3exmidlemwe  4671  sotri3  5127  funtpg  5372  fnprg  5376  fntpg  5377  funimaexglem  5404  fnco  5431  fvun1  5702  oprssov  6153  caovimo  6205  rdgivallem  6533  fnsnsplitdc  6659  funresdfunsndc  6660  f1dom2g  6915  mapxpen  7017  ssfidc  7110  sbthlemi4  7138  ordiso2  7213  updjud  7260  difinfsn  7278  mkvprop  7336  endjudisj  7403  distrnqg  7585  distrnq0  7657  prarloclem5  7698  cauappcvgprlemlol  7845  cauappcvgprlemupu  7847  caucvgprlemlol  7868  caucvgprlemupu  7870  caucvgprprlemlol  7896  caucvgprprlemupu  7898  cnegexlem2  8333  apcotr  8765  apadd1  8766  mulext1  8770  div2negap  8893  ltdiv2  9045  nndivtr  9163  difgtsumgt  9527  zdivmul  9548  gtndiv  9553  fzind  9573  eluzuzle  9742  eluzp1p1  9760  peano2uz  9790  qdivcl  9850  irrmul  9854  ledivge1le  9934  xrre2  10029  xaddass  10077  xltadd1  10084  xlt2add  10088  ubioc1  10137  ubicc2  10193  zltaddlt1le  10215  uzsubsubfz  10255  elfz1b  10298  fzp1nel  10312  fz0fzdiffz0  10338  difelfzle  10342  elfzo0  10394  elfzonlteqm1  10428  fzonn0p1p1  10431  fzosplitprm1  10452  fzoshftral  10456  subfzo0  10460  ceiqle  10547  modqval  10558  modqvalr  10559  flqpmodeq  10561  modq0  10563  mulqmod0  10564  negqmod0  10565  modqge0  10566  modqlt  10567  modqelico  10568  modqdiffl  10569  modqmulnn  10576  modqvalp1  10577  modqmuladdnn0  10602  qnegmod  10603  addmodid  10606  q2submod  10619  modifeq2int  10620  modfzo0difsn  10629  addmodlteq  10632  mulsubdivbinom2ap  10945  omgadd  11036  hashun  11039  ccatass  11156  lswccatn0lsw  11159  ccats1val2  11186  swrd00g  11196  swrdval2  11198  swrdlen  11199  swrdfv  11200  swrdfv0  11201  swrdnd  11206  swrdlen2  11209  swrdfv2  11210  swrdsbslen  11213  swrdspsleq  11214  ccatswrd  11217  pfxfv  11231  pfxn0  11235  pfxnd  11236  pfxsuff1eqwrdeq  11246  pfxpfx  11255  ccats1pfxeq  11261  ccatopth2  11264  wrd2ind  11270  pfxccatin12lem3  11279  pfxccat3  11281  swrdccat  11282  pfxccat3a  11285  redivap  11400  imdivap  11407  xrmaxltsup  11784  xrmaxadd  11787  xrlemininf  11797  xrminltinf  11798  climuni  11819  mulcn2  11838  fsumsplitsnun  11945  prodfap0  12071  fprodabs  12142  efsub  12207  cos12dec  12294  dvdsmodexp  12321  summodnegmod  12348  divalglemex  12448  divalg  12450  modremain  12455  ndvdssub  12456  fldivndvdslt  12463  bitsfzo  12481  nndvdslegcd  12501  dfgcd2  12550  mulgcd  12552  mulgcdr  12554  gcddiv  12555  rplpwr  12563  rppwr  12564  qredeq  12633  divgcdcoprmex  12639  cncongr1  12640  cncongr2  12641  pw2dvdslemn  12702  hashgcdlem  12775  modprm0  12792  modprmn0modprm0  12794  pythagtriplem1  12803  pythagtriplem3  12805  pythagtriplem10  12807  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem11  12812  pythagtriplem12  12813  pythagtriplem13  12814  pythagtriplem14  12815  pythagtriplem19  12820  pythagtrip  12821  dvdsprmpweqnn  12874  difsqpwdvds  12876  pcfaclem  12887  pcbc  12889  unennn  12983  ptex  13312  imasaddvallemg  13363  fvprif  13391  mgmsscl  13409  insubm  13533  mulginvcom  13699  mulgassr  13712  mulgmodid  13713  quselbasg  13782  ghmnsgima  13820  ringrng  14014  rmodislmodlem  14329  rmodislmod  14330  lssincl  14364  sralmod  14429  rnglidlmmgm  14475  rnglidlmsgrp  14476  rnglidlrng  14477  2idlcpblrng  14502  psrbaglesuppg  14651  ntrin  14813  elnei  14841  restco  14863  cnpnei  14908  cncnp2m  14920  sslm  14936  upxp  14961  blres  15123  metcnp3  15200  tgqioo  15244  dvply1  15454  ptolemy  15513  cxpcom  15627  logbgcd1irr  15656  logbprmirr  15661  lgslem1  15694  lgsneg  15718  lgsdilem  15721  lgsdir  15729  lgssq2  15735  lgsdirnn0  15741  gausslemma2dlem1a  15752  2lgslem1a1  15780  incistruhgr  15905  upgrex  15918  uhgr2edg  16019  iedginwlk  16098  uspgr2wlkeq2  16107  umgrclwwlkge2  16139