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  2789  ceqsralt  2790  vtoclgft  2814  ifbothdc  3595  ifnebibdc  3605  tpssi  3790  sotricim  4359  elirr  4578  en2lp  4591  reg3exmidlemwe  4616  sotri2  5068  poltletr  5071  funprg  5309  funtpg  5310  fntpg  5315  funimaexglem  5342  fvun1  5630  ftpg  5749  fsnunf  5765  fsnunfv  5766  caovimo  6121  brtposg  6321  smoel  6367  rdgivallem  6448  frecsuclem  6473  mapxpen  6918  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  sbthlemi4  7035  elfir  7048  updjud  7157  ltsopi  7406  distrnqg  7473  ltmnqg  7487  mulcanenq0ec  7531  distrnq0  7545  prarloclem5  7586  1idprl  7676  1idpru  7677  ltaprg  7705  recexprlemopl  7711  recexprlemopu  7713  recexprlem1ssl  7719  aptipr  7727  ltmprr  7728  cauappcvgprlemlol  7733  cauappcvgprlemupu  7735  caucvgprlemlol  7756  caucvgprlemupu  7758  caucvgprprlemlol  7784  caucvgprprlemupu  7786  readdcan  8185  cnegexlem2  8221  addcan2  8226  ltadd2  8465  apreap  8633  ltmul1  8638  apcotr  8653  apadd1  8654  mulext1  8658  divdirap  8743  divcanap5  8760  ltdiv1  8914  lt2halves  9246  zdivmul  9435  eluzsub  9650  ledivge1le  9820  addlelt  9862  xaddass  9963  xleadd1  9969  xltadd1  9970  elioo5  10027  iccsupr  10060  iccneg  10083  icoshft  10084  icoshftf1o  10085  zltaddlt1le  10101  fzen  10137  elfz1b  10184  fzrevral  10199  fzshftral  10202  elfz0ubfz0  10219  elfz0fzfz0  10220  fz0fzelfz0  10221  fz0fzdiffz0  10224  elfzo  10243  fzodcel  10247  elfzonlteqm1  10305  modqaddmulmod  10502  expdivap  10701  leexp2a  10703  bcval3  10862  omgadd  10913  shftfibg  11004  elicc4abs  11278  xrmaxltsup  11442  xrmaxadd  11445  xrlemininf  11455  xrminltinf  11456  mulcn2  11496  fsumsplitsnun  11603  prodfrecap  11730  demoivreALT  11958  dvdsval2  11974  dvdsmodexp  11979  dvdsmulcr  12005  modmulconst  12007  dvdsexp  12045  oddge22np1  12065  modremain  12113  mulgcd  12210  mulgcdr  12212  gcddiv  12213  rpmulgcd  12220  rplpwr  12221  coprmdvds  12287  cncongr1  12298  dvdsnprmd  12320  prmexpb  12346  rpexp  12348  cncongrprm  12352  modprm0  12450  modprmn0modprm0  12452  coprimeprodsq  12453  pythagtriplem1  12461  pythagtriplem3  12463  pythagtriplem10  12465  pythagtriplem6  12466  pythagtriplem11  12470  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem15  12474  pythagtriplem17  12476  pythagtriplem19  12478  pcdvdsb  12516  dvdsprmpweqle  12533  pcfaclem  12545  isstructr  12720  setsvala  12736  setsresg  12743  strle3g  12813  imasaddvallemg  13019  fvprif  13047  mgmsscl  13065  insubm  13189  dfgrp3mlem  13302  mulgdirlem  13361  mulgp1  13363  mulgmodid  13369  eqglact  13433  rngdi  13574  rngdir  13575  rmodislmodlem  13984  rmodislmod  13985  lssclg  13998  2idlcpblrng  14157  qusmulrng  14166  clsss  14462  ntrcls0  14475  neiss  14494  neipsm  14498  cnpnei  14563  cncnp2m  14575  cnconst2  14577  sslm  14591  upxp  14616  txmetcn  14863  ptolemy  15168  sincosq1eq  15183  rplogbval  15289  rpcxplogb  15308  lgsdirprm  15383  lgsdirnn0  15396  gausslemma2dlem1a  15407  gausslemma2dlem3  15412  2lgslem1a1  15435  2lgsoddprmlem1  15454  2lgsoddprmlem2  15455  findset  15699