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  5369  fvun1  5630  oprssov  6069  caovimo  6121  rdgivallem  6448  fnsnsplitdc  6572  funresdfunsndc  6573  f1dom2g  6824  mapxpen  6918  ssfidc  7007  sbthlemi4  7035  ordiso2  7110  updjud  7157  difinfsn  7175  mkvprop  7233  endjudisj  7295  distrnqg  7473  distrnq0  7545  prarloclem5  7586  cauappcvgprlemlol  7733  cauappcvgprlemupu  7735  caucvgprlemlol  7756  caucvgprlemupu  7758  caucvgprprlemlol  7784  caucvgprprlemupu  7786  cnegexlem2  8221  apcotr  8653  apadd1  8654  mulext1  8658  div2negap  8781  ltdiv2  8933  nndivtr  9051  difgtsumgt  9414  zdivmul  9435  gtndiv  9440  fzind  9460  eluzuzle  9628  eluzp1p1  9646  peano2uz  9676  qdivcl  9736  irrmul  9740  ledivge1le  9820  xrre2  9915  xaddass  9963  xltadd1  9970  xlt2add  9974  ubioc1  10023  ubicc2  10079  zltaddlt1le  10101  uzsubsubfz  10141  elfz1b  10184  fzp1nel  10198  fz0fzdiffz0  10224  difelfzle  10228  elfzo0  10277  elfzonlteqm1  10305  fzonn0p1p1  10308  fzosplitprm1  10329  fzoshftral  10333  subfzo0  10337  ceiqle  10424  modqval  10435  modqvalr  10436  flqpmodeq  10438  modq0  10440  mulqmod0  10441  negqmod0  10442  modqge0  10443  modqlt  10444  modqelico  10445  modqdiffl  10446  modqmulnn  10453  modqvalp1  10454  modqmuladdnn0  10479  qnegmod  10480  addmodid  10483  q2submod  10496  modifeq2int  10497  modfzo0difsn  10506  addmodlteq  10509  mulsubdivbinom2ap  10822  omgadd  10913  hashun  10916  redivap  11058  imdivap  11065  xrmaxltsup  11442  xrmaxadd  11445  xrlemininf  11455  xrminltinf  11456  climuni  11477  mulcn2  11496  fsumsplitsnun  11603  prodfap0  11729  fprodabs  11800  efsub  11865  cos12dec  11952  dvdsmodexp  11979  summodnegmod  12006  divalglemex  12106  divalg  12108  modremain  12113  ndvdssub  12114  fldivndvdslt  12121  bitsfzo  12139  nndvdslegcd  12159  dfgcd2  12208  mulgcd  12210  mulgcdr  12212  gcddiv  12213  rplpwr  12221  rppwr  12222  qredeq  12291  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  pw2dvdslemn  12360  hashgcdlem  12433  modprm0  12450  modprmn0modprm0  12452  pythagtriplem1  12461  pythagtriplem3  12463  pythagtriplem10  12465  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem11  12470  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem14  12473  pythagtriplem19  12478  pythagtrip  12479  dvdsprmpweqnn  12532  difsqpwdvds  12534  pcfaclem  12545  pcbc  12547  unennn  12641  ptex  12968  imasaddvallemg  13019  fvprif  13047  mgmsscl  13065  insubm  13189  mulginvcom  13355  mulgassr  13368  mulgmodid  13369  quselbasg  13438  ghmnsgima  13476  ringrng  13670  rmodislmodlem  13984  rmodislmod  13985  lssincl  14019  sralmod  14084  rnglidlmmgm  14130  rnglidlmsgrp  14131  rnglidlrng  14132  2idlcpblrng  14157  psrbaglesuppg  14306  ntrin  14468  elnei  14496  restco  14518  cnpnei  14563  cncnp2m  14575  sslm  14591  upxp  14616  blres  14778  metcnp3  14855  tgqioo  14899  dvply1  15109  ptolemy  15168  cxpcom  15282  logbgcd1irr  15311  logbprmirr  15316  lgslem1  15349  lgsneg  15373  lgsdilem  15376  lgsdir  15384  lgssq2  15390  lgsdirnn0  15396  gausslemma2dlem1a  15407  2lgslem1a1  15435