![]() |
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 4906 pssnn 9164 pssnnOLD 9261 suppeqfsuppbi 9373 infsupprpr 9495 axdc3lem2 10442 ltexprlem7 11033 nn01to3 12921 xrsupsslem 13282 xrinfmsslem 13283 injresinjlem 13748 injresinj 13749 addmodlteq 13907 ssnn0fi 13946 fsuppmapnn0fiubex 13953 fsuppmapnn0fiub0 13954 nn0o1gt2 16320 cshwsidrepswmod0 17024 symgextf1 19283 psgnunilem4 19359 cmpsublem 22894 aalioulem5 25840 gausslemma2dlem0i 26856 2lgsoddprm 26908 axlowdimlem15 28203 nbusgrvtxm1 28625 nb3grprlem1 28626 lfgrwlkprop 28933 frgrnbnb 29535 frgrwopreglem4a 29552 frgrwopreg 29565 nnn1suc 41177 volicorescl 45255 iccpartiltu 46076 odz2prm2pw 46217 prmdvdsfmtnof1lem2 46239 nnsum3primesle9 46448 bgoldbtbndlem1 46459 lindslinindsimp2lem5 47096 elfzolborelfzop1 47153 nn0sumshdiglemB 47259 |
Copyright terms: Public domain | W3C validator |