Theorem 3ad2ant3 1015

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 275	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜒)
3	2	3adant1 1010	1 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  simp3l  1020  simp3r  1021  simp31  1028  simp32  1029  simp33  1030  simp3ll  1063  simp3lr  1064  simp3rl  1065  simp3rr  1066  simp3l1  1097  simp3l2  1098  simp3l3  1099  simp3r1  1100  simp3r2  1101  simp3r3  1102  simp31l  1115  simp31r  1116  simp32l  1117  simp32r  1118  simp33l  1119  simp33r  1120  simp311  1139  simp312  1140  simp313  1141  simp321  1142  simp322  1143  simp323  1144  simp331  1145  simp332  1146  simp333  1147  3anim123i  1179  3jaao  1303  ceqsalt  2756  ceqsralt  2757  vtoclgft  2780  ifbothdc  3557  tpssi  3744  sotricim  4306  elirr  4523  en2lp  4536  reg3exmidlemwe  4561  sotri2  5006  poltletr  5009  funprg  5246  funtpg  5247  fntpg  5252  funimaexglem  5279  fvun1  5560  ftpg  5677  fsnunf  5693  fsnunfv  5694  caovimo  6043  brtposg  6230  smoel  6276  rdgivallem  6357  frecsuclem  6382  mapxpen  6822  unsnfi  6892  unsnfidcex  6893  unsnfidcel  6894  sbthlemi4  6933  elfir  6946  updjud  7055  ltsopi  7269  distrnqg  7336  ltmnqg  7350  mulcanenq0ec  7394  distrnq0  7408  prarloclem5  7449  1idprl  7539  1idpru  7540  ltaprg  7568  recexprlemopl  7574  recexprlemopu  7576  recexprlem1ssl  7582  aptipr  7590  ltmprr  7591  cauappcvgprlemlol  7596  cauappcvgprlemupu  7598  caucvgprlemlol  7619  caucvgprlemupu  7621  caucvgprprlemlol  7647  caucvgprprlemupu  7649  readdcan  8046  cnegexlem2  8082  addcan2  8087  ltadd2  8325  apreap  8493  ltmul1  8498  apcotr  8513  apadd1  8514  mulext1  8518  divdirap  8601  divcanap5  8618  ltdiv1  8771  lt2halves  9100  zdivmul  9289  eluzsub  9503  ledivge1le  9670  addlelt  9712  xaddass  9813  xleadd1  9819  xltadd1  9820  elioo5  9877  iccsupr  9910  iccneg  9933  icoshft  9934  icoshftf1o  9935  zltaddlt1le  9951  fzen  9986  elfz1b  10033  fzrevral  10048  fzshftral  10051  elfz0ubfz0  10068  elfz0fzfz0  10069  fz0fzelfz0  10070  fz0fzdiffz0  10073  elfzo  10092  fzodcel  10095  elfzonlteqm1  10153  modqaddmulmod  10334  expdivap  10514  leexp2a  10516  bcval3  10672  omgadd  10724  shftfibg  10771  elicc4abs  11045  xrmaxltsup  11208  xrmaxadd  11211  xrlemininf  11221  xrminltinf  11222  mulcn2  11262  fsumsplitsnun  11369  prodfrecap  11496  demoivreALT  11723  dvdsval2  11739  dvdsmodexp  11744  dvdsmulcr  11770  modmulconst  11772  dvdsexp  11808  oddge22np1  11827  modremain  11875  mulgcd  11958  mulgcdr  11960  gcddiv  11961  rpmulgcd  11968  rplpwr  11969  coprmdvds  12033  cncongr1  12044  dvdsnprmd  12066  prmexpb  12092  rpexp  12094  cncongrprm  12098  modprm0  12195  modprmn0modprm0  12197  coprimeprodsq  12198  pythagtriplem1  12206  pythagtriplem3  12208  pythagtriplem10  12210  pythagtriplem6  12211  pythagtriplem11  12215  pythagtriplem12  12216  pythagtriplem13  12217  pythagtriplem15  12219  pythagtriplem17  12221  pythagtriplem19  12223  pcdvdsb  12260  dvdsprmpweqle  12277  pcfaclem  12288  isstructr  12418  setsvala  12434  setsresg  12441  strle3g  12497  mgmsscl  12602  insubm  12690  clsss  12871  ntrcls0  12884  neiss  12903  neipsm  12907  cnpnei  12972  cncnp2m  12984  cnconst2  12986  sslm  13000  upxp  13025  txmetcn  13272  ptolemy  13498  sincosq1eq  13513  rplogbval  13616  rpcxplogb  13635  lgsdirprm  13688  lgsdirnn0  13701  findset  13940