Theorem adantrr 312

Description: Deduction adding a conjunct to an antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 ⊢ ((φ ∧ ψ) → χ)
2	1	exp 291	. . 3 ⊢ (φ → (ψ → χ))
3	2	adantrd 308	. 2 ⊢ (φ → ((ψ ∧ θ) → χ))
4	3	imp 277	1 ⊢ ((φ ∧ (ψ ∧ θ)) → χ)

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  anabss1 381  sbcom 916  po2nr 2135  sotric 2148  supmo 2156  dfwe2 2187  wereu 2197  tz7.7 2224  ordsucun 2333  f1oco 2816  f1ocnvfvb 2922  isocnv 2934  isotr 2935  isotrALT 2936  isomin 2937  isoini 2938  tfrlem8 2956  caoprmo 3084  oalim 3135  omlim 3136  oaass 3163  omordi 3164  oen0 3165  dom2d 3307  ssenen 3399  ssfi 3430  inf3lem6 3469  aceq5lem4 3561  aceq6b 3565  axacndlem4 3756  ordpipq 3850  ltapq 3870  ltmpq 3871  ltexpq 3874  genpnnp 3902  distrlem4pr 3924  ltexprlem6 3941  ltexprlem7 3942  prlem936b 3948  ltsrpr 3980  ssgt0sr 4011  axrecex 4079  add4t 4127  mul4t 4177  divadddivt 4264  divdivdivt 4265  divdiv23t 4271  zmax 4618  qaddclt 4642  qrecclt 4646  qbtwnre 4650  infxpidmlem7 4939  infxpidmlem12 4944  hvadd4t 5013  hvsub4t 5014  chocuni 5179  occllem6 5185  shscl 5282  elspansn4t 5478  osumlem2 5531  osumlem3 5532  osumlem4 5533  spansncv 5542  5oalem2 5545  5oalem5 5548  5oalem6 5549  3oalem2 5553  stles 5682  strlem3a 5693  atom1d 5750  cvexchlem 5759  atcvatlem 5770  atcvat3 5774  atcvat4 5775  mdsymlem1 5776  mdsymlem3 5778  mdsymlem5 5780  mdsymlem6 5781  sumdmdlem 5786  sumdmd 5787

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org