Theorem 3ad2ant3 1046

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simp3l  1051  simp3r  1052  simp31  1059  simp32  1060  simp33  1061  simp3ll  1094  simp3lr  1095  simp3rl  1096  simp3rr  1097  simp3l1  1128  simp3l2  1129  simp3l3  1130  simp3r1  1131  simp3r2  1132  simp3r3  1133  simp31l  1146  simp31r  1147  simp32l  1148  simp32r  1149  simp33l  1150  simp33r  1151  simp311  1170  simp312  1171  simp313  1172  simp321  1173  simp322  1174  simp323  1175  simp331  1176  simp332  1177  simp333  1178  3anim123i  1210  3jaao  1344  ceqsalt  2829  ceqsralt  2830  vtoclgft  2854  ifbothdc  3640  ifnebibdc  3651  ssprsseq  3835  tpssi  3842  sotricim  4420  elirr  4639  en2lp  4652  reg3exmidlemwe  4677  sotri2  5134  poltletr  5137  funprg  5380  funtpg  5381  fntpg  5386  funimaexglem  5413  fvun1  5712  ftpg  5838  fsnunf  5854  fsnunfv  5855  caovimo  6216  brtposg  6420  smoel  6466  rdgivallem  6547  frecsuclem  6572  domssr  6951  mapxpen  7034  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  sbthlemi4  7159  elfir  7172  updjud  7281  ltsopi  7540  distrnqg  7607  ltmnqg  7621  mulcanenq0ec  7665  distrnq0  7679  prarloclem5  7720  1idprl  7810  1idpru  7811  ltaprg  7839  recexprlemopl  7845  recexprlemopu  7847  recexprlem1ssl  7853  aptipr  7861  ltmprr  7862  cauappcvgprlemlol  7867  cauappcvgprlemupu  7869  caucvgprlemlol  7890  caucvgprlemupu  7892  caucvgprprlemlol  7918  caucvgprprlemupu  7920  readdcan  8319  cnegexlem2  8355  addcan2  8360  ltadd2  8599  apreap  8767  ltmul1  8772  apcotr  8787  apadd1  8788  mulext1  8792  divdirap  8877  divcanap5  8894  ltdiv1  9048  lt2halves  9380  zdivmul  9570  eluzsub  9786  ledivge1le  9961  addlelt  10003  xaddass  10104  xleadd1  10110  xltadd1  10111  elioo5  10168  iccsupr  10201  iccneg  10224  icoshft  10225  icoshftf1o  10226  zltaddlt1le  10242  fzen  10278  elfz1b  10325  fzrevral  10340  fzshftral  10343  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzo  10384  fzodcel  10388  elfzonlteqm1  10456  modqaddmulmod  10654  expdivap  10853  leexp2a  10855  bcval3  11014  omgadd  11066  ccatval1  11178  ccatval2  11179  ccatval3  11180  ccatass  11189  ccats1val2  11221  swrdval2  11236  swrdlen  11237  pfxfv  11269  pfxnd  11274  pfxsuffeqwrdeq  11283  swrdswrdlem  11289  swrdswrd  11290  pfxswrd  11291  pfxpfx  11293  ccats1pfxeq  11299  ccats1pfxeqrex  11300  pfxccatin12lem2  11316  pfxccatpfx1  11321  swrdccat3b  11325  pfxccatid  11326  shftfibg  11385  elicc4abs  11659  xrmaxltsup  11823  xrmaxadd  11826  xrlemininf  11836  xrminltinf  11837  mulcn2  11877  fsumsplitsnun  11985  prodfrecap  12112  demoivreALT  12340  dvdsval2  12356  dvdsmodexp  12361  dvdsmulcr  12387  modmulconst  12389  dvdsexp  12427  oddge22np1  12447  modremain  12495  mulgcd  12592  mulgcdr  12594  gcddiv  12595  rpmulgcd  12602  rplpwr  12603  coprmdvds  12669  cncongr1  12680  dvdsnprmd  12702  prmexpb  12728  rpexp  12730  cncongrprm  12734  modprm0  12832  modprmn0modprm0  12834  coprimeprodsq  12835  pythagtriplem1  12843  pythagtriplem3  12845  pythagtriplem10  12847  pythagtriplem6  12848  pythagtriplem11  12852  pythagtriplem12  12853  pythagtriplem13  12854  pythagtriplem15  12856  pythagtriplem17  12858  pythagtriplem19  12860  pcdvdsb  12898  dvdsprmpweqle  12915  pcfaclem  12927  isstructr  13102  setsvala  13118  setsresg  13125  strle3g  13196  imasaddvallemg  13403  fvprif  13431  mgmsscl  13449  insubm  13573  dfgrp3mlem  13686  mulgdirlem  13745  mulgp1  13747  mulgmodid  13753  eqglact  13817  rngdi  13959  rngdir  13960  rmodislmodlem  14370  rmodislmod  14371  lssclg  14384  2idlcpblrng  14543  qusmulrng  14552  clsss  14848  ntrcls0  14861  neiss  14880  neipsm  14884  cnpnei  14949  cncnp2m  14961  cnconst2  14963  sslm  14977  upxp  15002  txmetcn  15249  ptolemy  15554  sincosq1eq  15569  rplogbval  15675  rpcxplogb  15694  lgsdirprm  15769  lgsdirnn0  15782  gausslemma2dlem1a  15793  gausslemma2dlem3  15798  2lgslem1a1  15821  2lgsoddprmlem1  15840  2lgsoddprmlem2  15841  structiedg0val  15897  lpvtx  15936  incistruhgr  15947  upgredg2vtx  16005  upgredgpr  16006  ausgrumgrien  16027  ausgrusgrien  16028  ushgredgedg  16083  ushgredgedgloop  16085  uhgrissubgr  16118  egrsubgr  16120  0uhgrsubgr  16122  wlkvtxeledgg  16201  wlkeq  16211  wlkl1loop  16215  uspgr2wlkeq  16222  uspgr2wlkeq2  16223  wlkres  16236  loopclwwlkn1b  16276  clwwlkext2edg  16279  clwwlknonex2lem2  16295  clwwlknonex2  16296  clwwlknun  16298  eupth2lem3lem6fi  16328  findset  16566