Theorem adantrr 397

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
adant2.1	⊢ ((φ ⋀ ψ) → χ)

Assertion

Ref	Expression
adantrr	⊢ ((φ ⋀ (ψ ⋀ θ)) → χ)

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 ⊢ ((φ ⋀ ψ) → χ)
2	1	ex 373	. . 3 ⊢ (φ → (ψ → χ))
3	2	adantrd 393	. 2 ⊢ (φ → ((ψ ⋀ θ) → χ))
4	3	imp 350	1 ⊢ ((φ ⋀ (ψ ⋀ θ)) → χ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  ad2ant2r 411  ad2ant2lr 412  anabss1 502  3ad2antr1 816  sbcom 1262  ax11eq 1367  ax11el 1368  ifboth 2387  po2nr 2863  sotric 2876  tz7.7 2989  ordsucun 3098  opelxp1 3221  isocnv 3912  isomin 3915  isoini 3916  oalim 4183  omlim 4184  oaass 4211  omordi 4213  omwordri 4219  odi 4226  oen0 4229  oewordri 4235  oeworde 4236  dom2d 4422  ssenen 4524  ssfi 4556  inf3lem6 4635  rankxplim3 4731  aceq5lem4 4755  aceq6b 4759  unidom 4825  axacndlem4 4982  ltapq 5096  ltmpq 5097  ltexpq 5100  ltexprlem6 5167  ssgt0sr 5237  add4 5358  2addsub 5409  mul4 5440  muladd 5441  xrlttr 5573  ltleadd 5665  rec11r 5791  divdivdiv 5797  divdiv23 5804  lemul2a 5851  lemul12b 5854  ltmuldiv2 5877  ltdivmul 5879  ledivmul 5881  ltdivmul2 5883  ledivmul2 5886  lemuldiv2 5890  ltdiv23 5906  lediv23 5907  suprleub 6091  infmrcl 6101  xrsupsslem 6108  xrinfmsslem 6109  supxrunb1 6121  supxrunb2 6122  supxrleub 6131  zextlt 6225  zmax 6255  qbtwnre 6280  iooshf 6363  icounlem 6380  ioojoin 6384  recexp 6626  expsub 6629  expordi 6631  expord2 6635  sqlecan 6672  lenegsq 6917  seq1ublem 6943  fsumcom 7060  fsumshf 7063  2climnni 7134  2climnn0i 7135  climge0i 7144  climaddlem3 7148  climmullem1 7152  climmullem3 7154  climmullem5 7156  climmullem8 7159  climsqueezei 7172  climsqueeze2i 7173  climcaui 7188  serzf0i 7201  ser1f0i 7202  ser1cmp2i 7209  cvgratlem2 7283  cvgratlem5 7286  fsum0diaglem2 7289  mulc1cncf 7311  acdc3lem 7519  acdclem 7527  infxpidmlem7 7591  infxpidmlem12 7596  eltg2 7649  tgcl 7654  tgval3 7655  tgss2 7667  2basgen 7671  iscld 7695  ntrss 7714  ssnei2 7756  neindisj 7757  islp2 7773  cnpcl 7790  dnsconst 7814  ismsg 7826  blss 7879  blssex 7880  metcnp 7913  metcnpi3 7918  metcnpi4 7919  metcni2 7921  tgioolem 7940  lmss 7979  lmle 7986  metelcls 7991  metcnp4 7996  xplmi 7999  xpcn 8002  lmcau 8022  cmsss 8023  bcthlem11 8035  bcthlem15 8039  bcthlem18 8042  bcthlem19 8043  bcthlem20 8044  bcthlem21 8045  bcthlem24 8048  grpidinv 8078  grprcan 8088  grpinvid1 8097  grpinvid2 8098  grplcan 8100  abl4 8130  isring 8166  nvsubadd 8300  nvabs 8326  va1cnlem 8370  nvcnpi3 8447  nvcnpi4 8448  sspph 8540  ubthlem3 8556  ubthlem9 8562  ubthlem11 8564  ubthlem12 8565  ubthlem14 8567  hvadd4 8929  hvaddsub4 8969  chocunii 9196  occllem6 9202  shscli 9305  pjspansn 9524  fh1 9585  fh2 9586  cm2j 9587  spansncvi 9621  5oalem2 9624  5oalem5 9627  5oalem6 9628  3oalem2 9632  hoadd4 9734  cnvunop 9866  bralnfn 9896  eighmorth 9912  hmops 9969  hmopm 9970  hmopco 9972  lnopconi 9987  lnfnconi 10014  adjlnop 10043  adjmul 10049  adjadd 10050  nmopcoi 10052  kbass6 10078  hstle 10182  stlesi 10193  strlem3a 10204  hstrlem3a 10212  mdsl0 10262  mdexchi 10287  atom1d 10305  superpos 10306  cvexchlem 10320  atomli 10334  atcvatlem 10337  irredlem2 10343  irredlem3 10344  atcvat4i 10349  mdsymlem1 10355  mdsymlem3 10357  mdsymlem5 10359  mdsymlem6 10360  sumdmdlem 10370  sumdmdlem2 10371  cdj1i 10385  cdj3lem2b 10389  nndivsub 10446  iepiclem 10772

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain