Theorem 3ad2ant3 1023

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  simp3l  1028  simp3r  1029  simp31  1036  simp32  1037  simp33  1038  simp3ll  1071  simp3lr  1072  simp3rl  1073  simp3rr  1074  simp3l1  1105  simp3l2  1106  simp3l3  1107  simp3r1  1108  simp3r2  1109  simp3r3  1110  simp31l  1123  simp31r  1124  simp32l  1125  simp32r  1126  simp33l  1127  simp33r  1128  simp311  1147  simp312  1148  simp313  1149  simp321  1150  simp322  1151  simp323  1152  simp331  1153  simp332  1154  simp333  1155  3anim123i  1187  3jaao  1321  ceqsalt  2798  ceqsralt  2799  vtoclgft  2823  ifbothdc  3605  ifnebibdc  3615  tpssi  3800  sotricim  4370  elirr  4589  en2lp  4602  reg3exmidlemwe  4627  sotri2  5080  poltletr  5083  funprg  5324  funtpg  5325  fntpg  5330  funimaexglem  5357  fvun1  5645  ftpg  5768  fsnunf  5784  fsnunfv  5785  caovimo  6140  brtposg  6340  smoel  6386  rdgivallem  6467  frecsuclem  6492  domssr  6869  mapxpen  6945  unsnfi  7016  unsnfidcex  7017  unsnfidcel  7018  sbthlemi4  7062  elfir  7075  updjud  7184  ltsopi  7433  distrnqg  7500  ltmnqg  7514  mulcanenq0ec  7558  distrnq0  7572  prarloclem5  7613  1idprl  7703  1idpru  7704  ltaprg  7732  recexprlemopl  7738  recexprlemopu  7740  recexprlem1ssl  7746  aptipr  7754  ltmprr  7755  cauappcvgprlemlol  7760  cauappcvgprlemupu  7762  caucvgprlemlol  7783  caucvgprlemupu  7785  caucvgprprlemlol  7811  caucvgprprlemupu  7813  readdcan  8212  cnegexlem2  8248  addcan2  8253  ltadd2  8492  apreap  8660  ltmul1  8665  apcotr  8680  apadd1  8681  mulext1  8685  divdirap  8770  divcanap5  8787  ltdiv1  8941  lt2halves  9273  zdivmul  9463  eluzsub  9678  ledivge1le  9848  addlelt  9890  xaddass  9991  xleadd1  9997  xltadd1  9998  elioo5  10055  iccsupr  10088  iccneg  10111  icoshft  10112  icoshftf1o  10113  zltaddlt1le  10129  fzen  10165  elfz1b  10212  fzrevral  10227  fzshftral  10230  elfz0ubfz0  10247  elfz0fzfz0  10248  fz0fzelfz0  10249  fz0fzdiffz0  10252  elfzo  10271  fzodcel  10275  elfzonlteqm1  10339  modqaddmulmod  10536  expdivap  10735  leexp2a  10737  bcval3  10896  omgadd  10947  ccatval1  11053  ccatval2  11054  ccatval3  11055  ccatass  11064  ccats1val2  11092  swrdval2  11104  swrdlen  11105  shftfibg  11131  elicc4abs  11405  xrmaxltsup  11569  xrmaxadd  11572  xrlemininf  11582  xrminltinf  11583  mulcn2  11623  fsumsplitsnun  11730  prodfrecap  11857  demoivreALT  12085  dvdsval2  12101  dvdsmodexp  12106  dvdsmulcr  12132  modmulconst  12134  dvdsexp  12172  oddge22np1  12192  modremain  12240  mulgcd  12337  mulgcdr  12339  gcddiv  12340  rpmulgcd  12347  rplpwr  12348  coprmdvds  12414  cncongr1  12425  dvdsnprmd  12447  prmexpb  12473  rpexp  12475  cncongrprm  12479  modprm0  12577  modprmn0modprm0  12579  coprimeprodsq  12580  pythagtriplem1  12588  pythagtriplem3  12590  pythagtriplem10  12592  pythagtriplem6  12593  pythagtriplem11  12597  pythagtriplem12  12598  pythagtriplem13  12599  pythagtriplem15  12601  pythagtriplem17  12603  pythagtriplem19  12605  pcdvdsb  12643  dvdsprmpweqle  12660  pcfaclem  12672  isstructr  12847  setsvala  12863  setsresg  12870  strle3g  12940  imasaddvallemg  13147  fvprif  13175  mgmsscl  13193  insubm  13317  dfgrp3mlem  13430  mulgdirlem  13489  mulgp1  13491  mulgmodid  13497  eqglact  13561  rngdi  13702  rngdir  13703  rmodislmodlem  14112  rmodislmod  14113  lssclg  14126  2idlcpblrng  14285  qusmulrng  14294  clsss  14590  ntrcls0  14603  neiss  14622  neipsm  14626  cnpnei  14691  cncnp2m  14703  cnconst2  14705  sslm  14719  upxp  14744  txmetcn  14991  ptolemy  15296  sincosq1eq  15311  rplogbval  15417  rpcxplogb  15436  lgsdirprm  15511  lgsdirnn0  15524  gausslemma2dlem1a  15535  gausslemma2dlem3  15540  2lgslem1a1  15563  2lgsoddprmlem1  15582  2lgsoddprmlem2  15583  structiedg0val  15637  findset  15881