![]() |
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 1366 3ecase 1474 3elpr2eq 4864 pssnn 9112 pssnnOLD 9209 suppeqfsuppbi 9319 infsupprpr 9440 axdc3lem2 10387 ltexprlem7 10978 nn01to3 12866 xrsupsslem 13226 xrinfmsslem 13227 injresinjlem 13692 injresinj 13693 addmodlteq 13851 ssnn0fi 13890 fsuppmapnn0fiubex 13897 fsuppmapnn0fiub0 13898 nn0o1gt2 16263 cshwsidrepswmod0 16967 symgextf1 19203 psgnunilem4 19279 cmpsublem 22750 aalioulem5 25696 gausslemma2dlem0i 26712 2lgsoddprm 26764 axlowdimlem15 27905 nbusgrvtxm1 28327 nb3grprlem1 28328 lfgrwlkprop 28635 frgrnbnb 29237 frgrwopreglem4a 29254 frgrwopreg 29267 nnn1suc 40768 volicorescl 44784 iccpartiltu 45604 odz2prm2pw 45745 prmdvdsfmtnof1lem2 45767 nnsum3primesle9 45976 bgoldbtbndlem1 45987 lindslinindsimp2lem5 46533 elfzolborelfzop1 46590 nn0sumshdiglemB 46696 |
Copyright terms: Public domain | W3C validator |