Theorem 3ad2ant2 1019

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  simp2l  1023  simp2r  1024  simp21  1030  simp22  1031  simp23  1032  simp2ll  1064  simp2lr  1065  simp2rl  1066  simp2rr  1067  simp2l1  1096  simp2l2  1097  simp2l3  1098  simp2r1  1099  simp2r2  1100  simp2r3  1101  simp21l  1114  simp21r  1115  simp22l  1116  simp22r  1117  simp23l  1118  simp23r  1119  simp211  1135  simp212  1136  simp213  1137  simp221  1138  simp222  1139  simp223  1140  simp231  1141  simp232  1142  simp233  1143  3anim123i  1184  3jaao  1308  ceqsalt  2763  vtoclgft  2787  vtoclegft  2809  ifbothdc  3567  frirrg  4349  elirr  4539  en2lp  4552  reg3exmidlemwe  4577  sotri3  5025  funtpg  5265  fnprg  5269  fntpg  5270  funimaexglem  5297  fnco  5322  fvun1  5580  oprssov  6012  caovimo  6064  rdgivallem  6378  fnsnsplitdc  6502  funresdfunsndc  6503  f1dom2g  6752  mapxpen  6844  ssfidc  6930  sbthlemi4  6955  ordiso2  7030  updjud  7077  difinfsn  7095  mkvprop  7152  endjudisj  7205  distrnqg  7382  distrnq0  7454  prarloclem5  7495  cauappcvgprlemlol  7642  cauappcvgprlemupu  7644  caucvgprlemlol  7665  caucvgprlemupu  7667  caucvgprprlemlol  7693  caucvgprprlemupu  7695  cnegexlem2  8128  apcotr  8559  apadd1  8560  mulext1  8564  div2negap  8687  ltdiv2  8839  nndivtr  8956  difgtsumgt  9317  zdivmul  9338  gtndiv  9343  fzind  9363  eluzuzle  9531  eluzp1p1  9548  peano2uz  9578  qdivcl  9638  irrmul  9642  ledivge1le  9721  xrre2  9816  xaddass  9864  xltadd1  9871  xlt2add  9875  ubioc1  9924  ubicc2  9980  zltaddlt1le  10002  uzsubsubfz  10041  elfz1b  10084  fzp1nel  10098  fz0fzdiffz0  10124  difelfzle  10128  elfzo0  10176  elfzonlteqm1  10204  fzonn0p1p1  10207  fzosplitprm1  10228  fzoshftral  10232  subfzo0  10236  ceiqle  10307  modqval  10318  modqvalr  10319  flqpmodeq  10321  modq0  10323  mulqmod0  10324  negqmod0  10325  modqge0  10326  modqlt  10327  modqelico  10328  modqdiffl  10329  modqmulnn  10336  modqvalp1  10337  modqmuladdnn0  10362  qnegmod  10363  addmodid  10366  q2submod  10379  modifeq2int  10380  modfzo0difsn  10389  addmodlteq  10392  omgadd  10774  hashun  10777  redivap  10875  imdivap  10882  xrmaxltsup  11258  xrmaxadd  11261  xrlemininf  11271  xrminltinf  11272  climuni  11293  mulcn2  11312  fsumsplitsnun  11419  prodfap0  11545  fprodabs  11616  efsub  11681  cos12dec  11767  dvdsmodexp  11794  summodnegmod  11821  divalglemex  11918  divalg  11920  modremain  11925  ndvdssub  11926  fldivndvdslt  11931  nndvdslegcd  11957  dfgcd2  12006  mulgcd  12008  mulgcdr  12010  gcddiv  12011  rplpwr  12019  rppwr  12020  qredeq  12087  divgcdcoprmex  12093  cncongr1  12094  cncongr2  12095  pw2dvdslemn  12156  hashgcdlem  12229  modprm0  12245  modprmn0modprm0  12247  pythagtriplem1  12256  pythagtriplem3  12258  pythagtriplem10  12260  pythagtriplem6  12261  pythagtriplem7  12262  pythagtriplem11  12265  pythagtriplem12  12266  pythagtriplem13  12267  pythagtriplem14  12268  pythagtriplem19  12273  pythagtrip  12274  dvdsprmpweqnn  12326  difsqpwdvds  12328  pcfaclem  12338  pcbc  12340  unennn  12389  mgmsscl  12711  insubm  12803  mulginvcom  12938  mulgassr  12951  mulgmodid  12952  ntrin  13486  elnei  13514  restco  13536  cnpnei  13581  cncnp2m  13593  sslm  13609  upxp  13634  blres  13796  metcnp3  13873  tgqioo  13909  ptolemy  14107  cxpcom  14219  logbgcd1irr  14247  logbprmirr  14252  lgslem1  14263  lgsneg  14287  lgsdilem  14290  lgsdir  14298  lgssq2  14304  lgsdirnn0  14310