Theorem 3ad2ant3 1022

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
3ad2ant3	⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantl 277	. 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:  simp3l  1027  simp3r  1028  simp31  1035  simp32  1036  simp33  1037  simp3ll  1070  simp3lr  1071  simp3rl  1072  simp3rr  1073  simp3l1  1104  simp3l2  1105  simp3l3  1106  simp3r1  1107  simp3r2  1108  simp3r3  1109  simp31l  1122  simp31r  1123  simp32l  1124  simp32r  1125  simp33l  1126  simp33r  1127  simp311  1146  simp312  1147  simp313  1148  simp321  1149  simp322  1150  simp323  1151  simp331  1152  simp332  1153  simp333  1154  3anim123i  1186  3jaao  1319  ceqsalt  2786  ceqsralt  2787  vtoclgft  2811  ifbothdc  3591  ifnebibdc  3601  tpssi  3786  sotricim  4355  elirr  4574  en2lp  4587  reg3exmidlemwe  4612  sotri2  5064  poltletr  5067  funprg  5305  funtpg  5306  fntpg  5311  funimaexglem  5338  fvun1  5624  ftpg  5743  fsnunf  5759  fsnunfv  5760  caovimo  6114  brtposg  6309  smoel  6355  rdgivallem  6436  frecsuclem  6461  mapxpen  6906  unsnfi  6977  unsnfidcex  6978  unsnfidcel  6979  sbthlemi4  7021  elfir  7034  updjud  7143  ltsopi  7382  distrnqg  7449  ltmnqg  7463  mulcanenq0ec  7507  distrnq0  7521  prarloclem5  7562  1idprl  7652  1idpru  7653  ltaprg  7681  recexprlemopl  7687  recexprlemopu  7689  recexprlem1ssl  7695  aptipr  7703  ltmprr  7704  cauappcvgprlemlol  7709  cauappcvgprlemupu  7711  caucvgprlemlol  7732  caucvgprlemupu  7734  caucvgprprlemlol  7760  caucvgprprlemupu  7762  readdcan  8161  cnegexlem2  8197  addcan2  8202  ltadd2  8440  apreap  8608  ltmul1  8613  apcotr  8628  apadd1  8629  mulext1  8633  divdirap  8718  divcanap5  8735  ltdiv1  8889  lt2halves  9221  zdivmul  9410  eluzsub  9625  ledivge1le  9795  addlelt  9837  xaddass  9938  xleadd1  9944  xltadd1  9945  elioo5  10002  iccsupr  10035  iccneg  10058  icoshft  10059  icoshftf1o  10060  zltaddlt1le  10076  fzen  10112  elfz1b  10159  fzrevral  10174  fzshftral  10177  elfz0ubfz0  10194  elfz0fzfz0  10195  fz0fzelfz0  10196  fz0fzdiffz0  10199  elfzo  10218  fzodcel  10222  elfzonlteqm1  10280  modqaddmulmod  10465  expdivap  10664  leexp2a  10666  bcval3  10825  omgadd  10876  shftfibg  10967  elicc4abs  11241  xrmaxltsup  11404  xrmaxadd  11407  xrlemininf  11417  xrminltinf  11418  mulcn2  11458  fsumsplitsnun  11565  prodfrecap  11692  demoivreALT  11920  dvdsval2  11936  dvdsmodexp  11941  dvdsmulcr  11967  modmulconst  11969  dvdsexp  12006  oddge22np1  12025  modremain  12073  mulgcd  12156  mulgcdr  12158  gcddiv  12159  rpmulgcd  12166  rplpwr  12167  coprmdvds  12233  cncongr1  12244  dvdsnprmd  12266  prmexpb  12292  rpexp  12294  cncongrprm  12298  modprm0  12395  modprmn0modprm0  12397  coprimeprodsq  12398  pythagtriplem1  12406  pythagtriplem3  12408  pythagtriplem10  12410  pythagtriplem6  12411  pythagtriplem11  12415  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem15  12419  pythagtriplem17  12421  pythagtriplem19  12423  pcdvdsb  12461  dvdsprmpweqle  12478  pcfaclem  12490  isstructr  12636  setsvala  12652  setsresg  12659  strle3g  12729  imasaddvallemg  12901  fvprif  12929  mgmsscl  12947  insubm  13060  dfgrp3mlem  13173  mulgdirlem  13226  mulgp1  13228  mulgmodid  13234  eqglact  13298  rngdi  13439  rngdir  13440  rmodislmodlem  13849  rmodislmod  13850  lssclg  13863  2idlcpblrng  14022  qusmulrng  14031  clsss  14297  ntrcls0  14310  neiss  14329  neipsm  14333  cnpnei  14398  cncnp2m  14410  cnconst2  14412  sslm  14426  upxp  14451  txmetcn  14698  ptolemy  15000  sincosq1eq  15015  rplogbval  15118  rpcxplogb  15137  lgsdirprm  15191  lgsdirnn0  15204  gausslemma2dlem1a  15215  gausslemma2dlem3  15220  2lgslem1a1  15243  2lgsoddprmlem1  15262  2lgsoddprmlem2  15263  findset  15507