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  1319  ceqsalt  2789  vtoclgft  2814  vtoclegft  2836  ifbothdc  3595  ifnebibdc  3605  frirrg  4386  elirr  4578  en2lp  4591  reg3exmidlemwe  4616  sotri3  5069  funtpg  5310  fnprg  5314  fntpg  5315  funimaexglem  5342  fnco  5367  fvun1  5628  oprssov  6066  caovimo  6118  rdgivallem  6440  fnsnsplitdc  6564  funresdfunsndc  6565  f1dom2g  6816  mapxpen  6910  ssfidc  6999  sbthlemi4  7027  ordiso2  7102  updjud  7149  difinfsn  7167  mkvprop  7225  endjudisj  7279  distrnqg  7456  distrnq0  7528  prarloclem5  7569  cauappcvgprlemlol  7716  cauappcvgprlemupu  7718  caucvgprlemlol  7739  caucvgprlemupu  7741  caucvgprprlemlol  7767  caucvgprprlemupu  7769  cnegexlem2  8204  apcotr  8636  apadd1  8637  mulext1  8641  div2negap  8764  ltdiv2  8916  nndivtr  9034  difgtsumgt  9397  zdivmul  9418  gtndiv  9423  fzind  9443  eluzuzle  9611  eluzp1p1  9629  peano2uz  9659  qdivcl  9719  irrmul  9723  ledivge1le  9803  xrre2  9898  xaddass  9946  xltadd1  9953  xlt2add  9957  ubioc1  10006  ubicc2  10062  zltaddlt1le  10084  uzsubsubfz  10124  elfz1b  10167  fzp1nel  10181  fz0fzdiffz0  10207  difelfzle  10211  elfzo0  10260  elfzonlteqm1  10288  fzonn0p1p1  10291  fzosplitprm1  10312  fzoshftral  10316  subfzo0  10320  ceiqle  10407  modqval  10418  modqvalr  10419  flqpmodeq  10421  modq0  10423  mulqmod0  10424  negqmod0  10425  modqge0  10426  modqlt  10427  modqelico  10428  modqdiffl  10429  modqmulnn  10436  modqvalp1  10437  modqmuladdnn0  10462  qnegmod  10463  addmodid  10466  q2submod  10479  modifeq2int  10480  modfzo0difsn  10489  addmodlteq  10492  mulsubdivbinom2ap  10805  omgadd  10896  hashun  10899  redivap  11041  imdivap  11048  xrmaxltsup  11425  xrmaxadd  11428  xrlemininf  11438  xrminltinf  11439  climuni  11460  mulcn2  11479  fsumsplitsnun  11586  prodfap0  11712  fprodabs  11783  efsub  11848  cos12dec  11935  dvdsmodexp  11962  summodnegmod  11989  divalglemex  12089  divalg  12091  modremain  12096  ndvdssub  12097  fldivndvdslt  12104  bitsfzo  12122  nndvdslegcd  12142  dfgcd2  12191  mulgcd  12193  mulgcdr  12195  gcddiv  12196  rplpwr  12204  rppwr  12205  qredeq  12274  divgcdcoprmex  12280  cncongr1  12281  cncongr2  12282  pw2dvdslemn  12343  hashgcdlem  12416  modprm0  12433  modprmn0modprm0  12435  pythagtriplem1  12444  pythagtriplem3  12446  pythagtriplem10  12448  pythagtriplem6  12449  pythagtriplem7  12450  pythagtriplem11  12453  pythagtriplem12  12454  pythagtriplem13  12455  pythagtriplem14  12456  pythagtriplem19  12461  pythagtrip  12462  dvdsprmpweqnn  12515  difsqpwdvds  12517  pcfaclem  12528  pcbc  12530  unennn  12624  ptex  12945  imasaddvallemg  12968  fvprif  12996  mgmsscl  13014  insubm  13127  mulginvcom  13287  mulgassr  13300  mulgmodid  13301  quselbasg  13370  ghmnsgima  13408  ringrng  13602  rmodislmodlem  13916  rmodislmod  13917  lssincl  13951  sralmod  14016  rnglidlmmgm  14062  rnglidlmsgrp  14063  rnglidlrng  14064  2idlcpblrng  14089  psrbaglesuppg  14236  ntrin  14370  elnei  14398  restco  14420  cnpnei  14465  cncnp2m  14477  sslm  14493  upxp  14518  blres  14680  metcnp3  14757  tgqioo  14801  dvply1  15011  ptolemy  15070  cxpcom  15184  logbgcd1irr  15213  logbprmirr  15218  lgslem1  15251  lgsneg  15275  lgsdilem  15278  lgsdir  15286  lgssq2  15292  lgsdirnn0  15298  gausslemma2dlem1a  15309  2lgslem1a1  15337