![]() |
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 4869 pssnn 9119 pssnnOLD 9216 suppeqfsuppbi 9326 infsupprpr 9447 axdc3lem2 10394 ltexprlem7 10985 nn01to3 12873 xrsupsslem 13233 xrinfmsslem 13234 injresinjlem 13699 injresinj 13700 addmodlteq 13858 ssnn0fi 13897 fsuppmapnn0fiubex 13904 fsuppmapnn0fiub0 13905 nn0o1gt2 16270 cshwsidrepswmod0 16974 symgextf1 19210 psgnunilem4 19286 cmpsublem 22766 aalioulem5 25712 gausslemma2dlem0i 26728 2lgsoddprm 26780 axlowdimlem15 27947 nbusgrvtxm1 28369 nb3grprlem1 28370 lfgrwlkprop 28677 frgrnbnb 29279 frgrwopreglem4a 29296 frgrwopreg 29309 nnn1suc 40811 volicorescl 44868 iccpartiltu 45688 odz2prm2pw 45829 prmdvdsfmtnof1lem2 45851 nnsum3primesle9 46060 bgoldbtbndlem1 46071 lindslinindsimp2lem5 46617 elfzolborelfzop1 46674 nn0sumshdiglemB 46780 |
Copyright terms: Public domain | W3C validator |