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 1368 3ecase 1476 3elpr2eq 4815 pssnn 8843 pssnnOLD 8892 suppeqfsuppbi 8996 infsupprpr 9117 axdc3lem2 10062 ltexprlem7 10653 nn01to3 12534 xrsupsslem 12894 xrinfmsslem 12895 injresinjlem 13359 injresinj 13360 addmodlteq 13516 ssnn0fi 13555 fsuppmapnn0fiubex 13562 fsuppmapnn0fiub0 13563 nn0o1gt2 15939 cshwsidrepswmod0 16645 symgextf1 18810 psgnunilem4 18886 cmpsublem 22293 aalioulem5 25226 gausslemma2dlem0i 26242 2lgsoddprm 26294 axlowdimlem15 27044 nbusgrvtxm1 27464 nb3grprlem1 27465 lfgrwlkprop 27772 frgrnbnb 28373 frgrwopreglem4a 28390 frgrwopreg 28403 nnn1suc 40001 volicorescl 43764 iccpartiltu 44545 odz2prm2pw 44686 prmdvdsfmtnof1lem2 44708 nnsum3primesle9 44917 bgoldbtbndlem1 44928 lindslinindsimp2lem5 45474 elfzolborelfzop1 45531 nn0sumshdiglemB 45637 |
Copyright terms: Public domain | W3C validator |