![]() |
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 1363 3ecase 1471 3elpr2eq 4912 pssnn 9206 pssnnOLD 9299 suppeqfsuppbi 9422 infsupprpr 9547 axdc3lem2 10494 ltexprlem7 11085 nn01to3 12977 xrsupsslem 13340 xrinfmsslem 13341 injresinjlem 13807 injresinj 13808 addmodlteq 13966 ssnn0fi 14005 fsuppmapnn0fiubex 14012 fsuppmapnn0fiub0 14013 nn0o1gt2 16383 cshwsidrepswmod0 17097 symgextf1 19419 psgnunilem4 19495 cmpsublem 23394 aalioulem5 26364 gausslemma2dlem0i 27393 2lgsoddprm 27445 axlowdimlem15 28890 nbusgrvtxm1 29315 nb3grprlem1 29316 lfgrwlkprop 29624 frgrnbnb 30226 frgrwopreglem4a 30243 frgrwopreg 30256 nnn1suc 42080 volicorescl 46174 iccpartiltu 46994 odz2prm2pw 47135 prmdvdsfmtnof1lem2 47157 nnsum3primesle9 47366 bgoldbtbndlem1 47377 clnbgrgrim 47481 lindslinindsimp2lem5 47845 elfzolborelfzop1 47902 nn0sumshdiglemB 48008 |
Copyright terms: Public domain | W3C validator |