Theorem adantlr 310

Description: Deduction adding a conjunct to an antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantlr

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

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  anabss5 384  supmo 2156  tz7.7 2224  onmindif2 2313  peano5 2394  fvco 2865  cleqfv 2880  isocnv 2934  isotr 2935  isotrALT 2936  caoprmo 3084  oaordi 3148  oawordri 3152  oaass 3163  omordi 3164  omsmolem 3195  omsmo 3196  xpdom2 3345  sbthlem9 3357  mapenlem1 3384  mapenlem2 3385  mapxpen 3390  xpmapenlem3 3393  xpmapenlem4 3394  fiint 3445  aceq5 3563  ac6lem 3575  zornlem6 3608  zornlem7 3609  fodom 3613  unxpdomlem 3649  axrepndlem2 3739  axrepnd 3740  axpowndlem2 3744  axacndlem5 3757  axacnd 3758  mulcanpi 3821  indpi 3828  genpnnp 3902  genpnmax 3904  addclprlem2 3913  mulclprlem 3915  distrlem4pr 3924  prlem934b 3932  ltexprlem7 3942  mulcmpblnr 3977  ssgt0sr 4011  divadddivt 4264  divdivdivt 4265  nnleltp1t 4448  zrevaddclt 4592  zltp1let 4597  uzwo2 4606  zbtwnre 4619  qaddclt 4642  qrecclt 4646  qrevaddclt 4648  qbtwnre 4650  expcllem 4682  expaddt 4698  sqr2irrlem3 4779  infxpidmlem1 4933  infxpidmlem11 4943  infxpidmlem12 4944  infmap2lem2 4952  hvsub4t 5014  chocuni 5179  occllem6 5185  projlem25 5217  projlem26 5218  projlem28 5220  shscl 5282  shsel1t 5286  spansncol 5473  elspansn4t 5478  osumlem2 5531  osumlem3 5532  osumlem4 5533  5oalem2 5545  5oalem4 5547  3oalem2 5553  pjss2co 5634  pj3s 5659  pj3cor1 5661  cvcon3t 5716  mdbr2 5728  dmdbr2 5733  atcvatlem 5770  mdsymlem1 5776  mdsymlem2 5777  mdsymlem3 5778  mdsymlem4 5779  mdsymlem5 5780  mdsymlem6 5781  sumdmdi 5785

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