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  7404  distrnqg  7471  ltmnqg  7485  mulcanenq0ec  7529  distrnq0  7543  prarloclem5  7584  1idprl  7674  1idpru  7675  ltaprg  7703  recexprlemopl  7709  recexprlemopu  7711  recexprlem1ssl  7717  aptipr  7725  ltmprr  7726  cauappcvgprlemlol  7731  cauappcvgprlemupu  7733  caucvgprlemlol  7754  caucvgprlemupu  7756  caucvgprprlemlol  7782  caucvgprprlemupu  7784  readdcan  8183  cnegexlem2  8219  addcan2  8224  ltadd2  8463  apreap  8631  ltmul1  8636  apcotr  8651  apadd1  8652  mulext1  8656  divdirap  8741  divcanap5  8758  ltdiv1  8912  lt2halves  9244  zdivmul  9433  eluzsub  9648  ledivge1le  9818  addlelt  9860  xaddass  9961  xleadd1  9967  xltadd1  9968  elioo5  10025  iccsupr  10058  iccneg  10081  icoshft  10082  icoshftf1o  10083  zltaddlt1le  10099  fzen  10135  elfz1b  10182  fzrevral  10197  fzshftral  10200  elfz0ubfz0  10217  elfz0fzfz0  10218  fz0fzelfz0  10219  fz0fzdiffz0  10222  elfzo  10241  fzodcel  10245  elfzonlteqm1  10303  modqaddmulmod  10500  expdivap  10699  leexp2a  10701  bcval3  10860  omgadd  10911  shftfibg  11002  elicc4abs  11276  xrmaxltsup  11440  xrmaxadd  11443  xrlemininf  11453  xrminltinf  11454  mulcn2  11494  fsumsplitsnun  11601  prodfrecap  11728  demoivreALT  11956  dvdsval2  11972  dvdsmodexp  11977  dvdsmulcr  12003  modmulconst  12005  dvdsexp  12043  oddge22np1  12063  modremain  12111  mulgcd  12208  mulgcdr  12210  gcddiv  12211  rpmulgcd  12218  rplpwr  12219  coprmdvds  12285  cncongr1  12296  dvdsnprmd  12318  prmexpb  12344  rpexp  12346  cncongrprm  12350  modprm0  12448  modprmn0modprm0  12450  coprimeprodsq  12451  pythagtriplem1  12459  pythagtriplem3  12461  pythagtriplem10  12463  pythagtriplem6  12464  pythagtriplem11  12468  pythagtriplem12  12469  pythagtriplem13  12470  pythagtriplem15  12472  pythagtriplem17  12474  pythagtriplem19  12476  pcdvdsb  12514  dvdsprmpweqle  12531  pcfaclem  12543  isstructr  12718  setsvala  12734  setsresg  12741  strle3g  12811  imasaddvallemg  13017  fvprif  13045  mgmsscl  13063  insubm  13187  dfgrp3mlem  13300  mulgdirlem  13359  mulgp1  13361  mulgmodid  13367  eqglact  13431  rngdi  13572  rngdir  13573  rmodislmodlem  13982  rmodislmod  13983  lssclg  13996  2idlcpblrng  14155  qusmulrng  14164  clsss  14438  ntrcls0  14451  neiss  14470  neipsm  14474  cnpnei  14539  cncnp2m  14551  cnconst2  14553  sslm  14567  upxp  14592  txmetcn  14839  ptolemy  15144  sincosq1eq  15159  rplogbval  15265  rpcxplogb  15284  lgsdirprm  15359  lgsdirnn0  15372  gausslemma2dlem1a  15383  gausslemma2dlem3  15388  2lgslem1a1  15411  2lgsoddprmlem1  15430  2lgsoddprmlem2  15431  findset  15675