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  shftfibg  11073  elicc4abs  11347  xrmaxltsup  11511  xrmaxadd  11514  xrlemininf  11524  xrminltinf  11525  mulcn2  11565  fsumsplitsnun  11672  prodfrecap  11799  demoivreALT  12027  dvdsval2  12043  dvdsmodexp  12048  dvdsmulcr  12074  modmulconst  12076  dvdsexp  12114  oddge22np1  12134  modremain  12182  mulgcd  12279  mulgcdr  12281  gcddiv  12282  rpmulgcd  12289  rplpwr  12290  coprmdvds  12356  cncongr1  12367  dvdsnprmd  12389  prmexpb  12415  rpexp  12417  cncongrprm  12421  modprm0  12519  modprmn0modprm0  12521  coprimeprodsq  12522  pythagtriplem1  12530  pythagtriplem3  12532  pythagtriplem10  12534  pythagtriplem6  12535  pythagtriplem11  12539  pythagtriplem12  12540  pythagtriplem13  12541  pythagtriplem15  12543  pythagtriplem17  12545  pythagtriplem19  12547  pcdvdsb  12585  dvdsprmpweqle  12602  pcfaclem  12614  isstructr  12789  setsvala  12805  setsresg  12812  strle3g  12882  imasaddvallemg  13089  fvprif  13117  mgmsscl  13135  insubm  13259  dfgrp3mlem  13372  mulgdirlem  13431  mulgp1  13433  mulgmodid  13439  eqglact  13503  rngdi  13644  rngdir  13645  rmodislmodlem  14054  rmodislmod  14055  lssclg  14068  2idlcpblrng  14227  qusmulrng  14236  clsss  14532  ntrcls0  14545  neiss  14564  neipsm  14568  cnpnei  14633  cncnp2m  14645  cnconst2  14647  sslm  14661  upxp  14686  txmetcn  14933  ptolemy  15238  sincosq1eq  15253  rplogbval  15359  rpcxplogb  15378  lgsdirprm  15453  lgsdirnn0  15466  gausslemma2dlem1a  15477  gausslemma2dlem3  15482  2lgslem1a1  15505  2lgsoddprmlem1  15524  2lgsoddprmlem2  15525  structiedg0val  15579  findset  15814