Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > a1dd | Structured version Visualization version GIF version |
Description: Double deduction introducing an antecedent. Deduction associated with a1d 25. Double deduction associated with ax-1 6 and a1i 11. (Contributed by NM, 17-Dec-2004.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.) |
Ref | Expression |
---|---|
a1dd.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
a1dd | ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a1dd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | ax-1 6 | . 2 ⊢ (𝜒 → (𝜃 → 𝜒)) | |
3 | 1, 2 | syl6 35 | 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: 2a1dd 51 merco2 1739 equvel 2456 propeqop 5421 funopsn 7020 xpexr 7765 omordi 8397 omwordi 8402 odi 8410 omass 8411 oen0 8417 oewordi 8422 oewordri 8423 nnmwordi 8466 omabs 8481 fisupg 9062 fiinfg 9258 cantnfle 9429 cantnflem1 9447 pr2ne 9761 gchina 10455 nqereu 10685 supsrlem 10867 1re 10975 lemul1a 11829 xlemul1a 13022 xrsupsslem 13041 xrinfmsslem 13042 xrub 13046 supxrunb1 13053 supxrunb2 13054 difelfzle 13369 addmodlteq 13666 seqcl2 13741 facdiv 14001 facwordi 14003 faclbnd 14004 pfxccat3 14447 dvdsabseq 16022 divgcdcoprm0 16370 2mulprm 16398 exprmfct 16409 prmfac1 16426 pockthg 16607 cply1mul 21465 mdetralt 21757 cmpsub 22551 fbfinnfr 22992 alexsubALTlem2 23199 alexsubALTlem3 23200 ovolicc2lem3 24683 fta1g 25332 fta1 25468 mulcxp 25840 cxpcn3lem 25900 gausslemma2dlem4 26517 colinearalg 27278 upgrwlkdvdelem 28104 umgr2wlk 28314 clwwlknwwlksn 28402 clwwlknonex2lem2 28472 dmdbr5ati 30784 cvmlift3lem4 33284 dfon2lem9 33767 fscgr 34382 colinbtwnle 34420 broutsideof2 34424 a1i14 34489 a1i24 34490 ordcmp 34636 bj-peircestab 34733 wl-aleq 35694 itg2addnc 35831 filbcmb 35898 mpobi123f 36320 mptbi12f 36324 ac6s6 36330 ltrnid 38149 cdleme25dN 38370 nn0rppwr 40333 ntrneiiso 41701 ee323 42128 vd13 42221 vd23 42222 ee03 42361 ee23an 42377 ee32 42379 ee32an 42381 ee123 42383 iccpartgt 44879 stgoldbwt 45228 tgoldbach 45269 nzerooringczr 45630 |
Copyright terms: Public domain | W3C validator |