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  1320  ceqsalt  2797  ceqsralt  2798  vtoclgft  2822  ifbothdc  3604  ifnebibdc  3614  tpssi  3799  sotricim  4369  elirr  4588  en2lp  4601  reg3exmidlemwe  4626  sotri2  5079  poltletr  5082  funprg  5323  funtpg  5324  fntpg  5329  funimaexglem  5356  fvun1  5644  ftpg  5767  fsnunf  5783  fsnunfv  5784  caovimo  6139  brtposg  6339  smoel  6385  rdgivallem  6466  frecsuclem  6491  domssr  6868  mapxpen  6944  unsnfi  7015  unsnfidcex  7016  unsnfidcel  7017  sbthlemi4  7061  elfir  7074  updjud  7183  ltsopi  7432  distrnqg  7499  ltmnqg  7513  mulcanenq0ec  7557  distrnq0  7571  prarloclem5  7612  1idprl  7702  1idpru  7703  ltaprg  7731  recexprlemopl  7737  recexprlemopu  7739  recexprlem1ssl  7745  aptipr  7753  ltmprr  7754  cauappcvgprlemlol  7759  cauappcvgprlemupu  7761  caucvgprlemlol  7782  caucvgprlemupu  7784  caucvgprprlemlol  7810  caucvgprprlemupu  7812  readdcan  8211  cnegexlem2  8247  addcan2  8252  ltadd2  8491  apreap  8659  ltmul1  8664  apcotr  8679  apadd1  8680  mulext1  8684  divdirap  8769  divcanap5  8786  ltdiv1  8940  lt2halves  9272  zdivmul  9462  eluzsub  9677  ledivge1le  9847  addlelt  9889  xaddass  9990  xleadd1  9996  xltadd1  9997  elioo5  10054  iccsupr  10087  iccneg  10110  icoshft  10111  icoshftf1o  10112  zltaddlt1le  10128  fzen  10164  elfz1b  10211  fzrevral  10226  fzshftral  10229  elfz0ubfz0  10246  elfz0fzfz0  10247  fz0fzelfz0  10248  fz0fzdiffz0  10251  elfzo  10270  fzodcel  10274  elfzonlteqm1  10337  modqaddmulmod  10534  expdivap  10733  leexp2a  10735  bcval3  10894  omgadd  10945  ccatval1  11051  ccatval2  11052  ccatval3  11053  ccatass  11062  ccats1val2  11090  shftfibg  11102  elicc4abs  11376  xrmaxltsup  11540  xrmaxadd  11543  xrlemininf  11553  xrminltinf  11554  mulcn2  11594  fsumsplitsnun  11701  prodfrecap  11828  demoivreALT  12056  dvdsval2  12072  dvdsmodexp  12077  dvdsmulcr  12103  modmulconst  12105  dvdsexp  12143  oddge22np1  12163  modremain  12211  mulgcd  12308  mulgcdr  12310  gcddiv  12311  rpmulgcd  12318  rplpwr  12319  coprmdvds  12385  cncongr1  12396  dvdsnprmd  12418  prmexpb  12444  rpexp  12446  cncongrprm  12450  modprm0  12548  modprmn0modprm0  12550  coprimeprodsq  12551  pythagtriplem1  12559  pythagtriplem3  12561  pythagtriplem10  12563  pythagtriplem6  12564  pythagtriplem11  12568  pythagtriplem12  12569  pythagtriplem13  12570  pythagtriplem15  12572  pythagtriplem17  12574  pythagtriplem19  12576  pcdvdsb  12614  dvdsprmpweqle  12631  pcfaclem  12643  isstructr  12818  setsvala  12834  setsresg  12841  strle3g  12911  imasaddvallemg  13118  fvprif  13146  mgmsscl  13164  insubm  13288  dfgrp3mlem  13401  mulgdirlem  13460  mulgp1  13462  mulgmodid  13468  eqglact  13532  rngdi  13673  rngdir  13674  rmodislmodlem  14083  rmodislmod  14084  lssclg  14097  2idlcpblrng  14256  qusmulrng  14265  clsss  14561  ntrcls0  14574  neiss  14593  neipsm  14597  cnpnei  14662  cncnp2m  14674  cnconst2  14676  sslm  14690  upxp  14715  txmetcn  14962  ptolemy  15267  sincosq1eq  15282  rplogbval  15388  rpcxplogb  15407  lgsdirprm  15482  lgsdirnn0  15495  gausslemma2dlem1a  15506  gausslemma2dlem3  15511  2lgslem1a1  15534  2lgsoddprmlem1  15553  2lgsoddprmlem2  15554  structiedg0val  15608  findset  15843