Theorem 3ad2ant3 1009

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

Syntax hints:   → wi 4   ∧ w3a 967

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 969

This theorem is referenced by:  simp3l  1014  simp3r  1015  simp31  1022  simp32  1023  simp33  1024  simp3ll  1057  simp3lr  1058  simp3rl  1059  simp3rr  1060  simp3l1  1091  simp3l2  1092  simp3l3  1093  simp3r1  1094  simp3r2  1095  simp3r3  1096  simp31l  1109  simp31r  1110  simp32l  1111  simp32r  1112  simp33l  1113  simp33r  1114  simp311  1133  simp312  1134  simp313  1135  simp321  1136  simp322  1137  simp323  1138  simp331  1139  simp332  1140  simp333  1141  3anim123i  1173  3jaao  1297  ceqsalt  2747  ceqsralt  2748  vtoclgft  2771  ifbothdc  3547  tpssi  3733  sotricim  4295  elirr  4512  en2lp  4525  reg3exmidlemwe  4550  sotri2  4995  poltletr  4998  funprg  5232  funtpg  5233  fntpg  5238  funimaexglem  5265  fvun1  5546  ftpg  5663  fsnunf  5679  fsnunfv  5680  caovimo  6026  brtposg  6213  smoel  6259  rdgivallem  6340  frecsuclem  6365  mapxpen  6805  unsnfi  6875  unsnfidcex  6876  unsnfidcel  6877  sbthlemi4  6916  elfir  6929  updjud  7038  ltsopi  7252  distrnqg  7319  ltmnqg  7333  mulcanenq0ec  7377  distrnq0  7391  prarloclem5  7432  1idprl  7522  1idpru  7523  ltaprg  7551  recexprlemopl  7557  recexprlemopu  7559  recexprlem1ssl  7565  aptipr  7573  ltmprr  7574  cauappcvgprlemlol  7579  cauappcvgprlemupu  7581  caucvgprlemlol  7602  caucvgprlemupu  7604  caucvgprprlemlol  7630  caucvgprprlemupu  7632  readdcan  8029  cnegexlem2  8065  addcan2  8070  ltadd2  8308  apreap  8476  ltmul1  8481  apcotr  8496  apadd1  8497  mulext1  8501  divdirap  8584  divcanap5  8601  ltdiv1  8754  lt2halves  9083  zdivmul  9272  eluzsub  9486  ledivge1le  9653  addlelt  9695  xaddass  9796  xleadd1  9802  xltadd1  9803  elioo5  9860  iccsupr  9893  iccneg  9916  icoshft  9917  icoshftf1o  9918  zltaddlt1le  9934  fzen  9968  elfz1b  10015  fzrevral  10030  fzshftral  10033  elfz0ubfz0  10050  elfz0fzfz0  10051  fz0fzelfz0  10052  fz0fzdiffz0  10055  elfzo  10074  fzodcel  10077  elfzonlteqm1  10135  modqaddmulmod  10316  expdivap  10496  leexp2a  10498  bcval3  10653  omgadd  10704  shftfibg  10748  elicc4abs  11022  xrmaxltsup  11185  xrmaxadd  11188  xrlemininf  11198  xrminltinf  11199  mulcn2  11239  fsumsplitsnun  11346  prodfrecap  11473  demoivreALT  11700  dvdsval2  11716  dvdsmodexp  11721  dvdsmulcr  11747  modmulconst  11749  dvdsexp  11784  oddge22np1  11803  modremain  11851  mulgcd  11934  mulgcdr  11936  gcddiv  11937  rpmulgcd  11944  rplpwr  11945  coprmdvds  12003  cncongr1  12014  dvdsnprmd  12036  prmexpb  12060  rpexp  12062  cncongrprm  12066  modprm0  12163  modprmn0modprm0  12165  coprimeprodsq  12166  pythagtriplem1  12174  pythagtriplem3  12176  pythagtriplem10  12178  pythagtriplem6  12179  pythagtriplem11  12183  pythagtriplem12  12184  pythagtriplem13  12185  pythagtriplem15  12187  pythagtriplem17  12189  pythagtriplem19  12191  pcdvdsb  12228  dvdsprmpweqle  12245  pcfaclem  12256  isstructr  12346  setsvala  12362  setsresg  12369  strle3g  12423  clsss  12659  ntrcls0  12672  neiss  12691  neipsm  12695  cnpnei  12760  cncnp2m  12772  cnconst2  12774  sslm  12788  upxp  12813  txmetcn  13060  ptolemy  13286  sincosq1eq  13301  rplogbval  13404  rpcxplogb  13423  findset  13662