|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 2a1d | Structured version Visualization version GIF version | ||
| Description: Deduction introducing two antecedents. Two applications of a1d 25. Deduction associated with 2a1 28 and 2a1i 12. (Contributed by BJ, 10-Aug-2020.) | 
| Ref | Expression | 
|---|---|
| 2a1d.1 | ⊢ (𝜑 → 𝜓) | 
| Ref | Expression | 
|---|---|
| 2a1d | ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜓))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 2a1d.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | 1 | a1d 25 | . 2 ⊢ (𝜑 → (𝜃 → 𝜓)) | 
| 3 | 2 | a1d 25 | 1 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜓))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 | 
| This theorem is referenced by: 2a1 28 ad5ant125 1367 3ecase 1475 3elpr2eq 4905 pssnn 9209 suppeqfsuppbi 9420 infsupprpr 9545 axdc3lem2 10492 ltexprlem7 11083 nn01to3 12984 xrsupsslem 13350 xrinfmsslem 13351 injresinjlem 13827 injresinj 13828 addmodlteq 13988 ssnn0fi 14027 fsuppmapnn0fiubex 14034 fsuppmapnn0fiub0 14035 nn0o1gt2 16419 cshwsidrepswmod0 17133 symgextf1 19440 psgnunilem4 19516 cmpsublem 23408 aalioulem5 26379 gausslemma2dlem0i 27409 2lgsoddprm 27461 axlowdimlem15 28972 nbusgrvtxm1 29397 nb3grprlem1 29398 lfgrwlkprop 29706 frgrnbnb 30313 frgrwopreglem4a 30330 frgrwopreg 30343 nnn1suc 42306 volicorescl 46573 iccpartiltu 47414 odz2prm2pw 47555 prmdvdsfmtnof1lem2 47577 nnsum3primesle9 47786 bgoldbtbndlem1 47797 clnbgrgrim 47907 grtriprop 47913 isgrtri 47915 grimgrtri 47921 grlimgrtri 47968 lindslinindsimp2lem5 48384 elfzolborelfzop1 48441 nn0sumshdiglemB 48546 | 
| Copyright terms: Public domain | W3C validator |