pm2.61d - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pm2.61d		Structured version Visualization version GIF version

Theorem pm2.61d 182

Description: Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)

**Hypotheses**
Ref	Expression
pm2.61d.1	⊢ (𝜑 → (𝜓 → 𝜒))
pm2.61d.2	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

**Assertion**
Ref	Expression
pm2.61d	⊢ (𝜑 → 𝜒)

**Proof of Theorem pm2.61d**
Step	Hyp	Ref	Expression
1		pm2.61d.2	. . . 4 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2	1	con1d 147	. . 3 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3		pm2.61d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	syld 47	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜒))
5	4	pm2.18d 127	1 ⊢ (𝜑 → 𝜒)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem is referenced by: pm2.61d1 183 pm2.61d2 184 pm5.21ndd 384 bija 385 pm2.61dan 812 ecase3d 1030 pm2.61dne 3073 ordunidif 6207 dff3 6843 tfindsg 7555 findsg 7590 brtpos 7884 omwordi 8180 omass 8189 nnmwordi 8244 pssnn 8720 frfi 8747 ixpiunwdom 9038 cantnfp1lem3 9127 infxpenlem 9424 infxp 9626 ackbij1lem16 9646 axpowndlem3 10010 pwfseqlem4a 10072 gchina 10110 prlem936 10458 supsrlem 10522 flflp1 13172 hashunx 13743 swrdccat3blem 14092 repswswrd 14137 sumss 15073 fsumss 15074 prodss 15293 fprodss 15294 ruclem2 15577 prmind2 16019 rpexp 16054 fermltl 16111 prmreclem5 16246 ramcl 16355 wunress 16556 divsfval 16812 efgsfo 18857 lt6abl 19008 gsumval3 19020 mdetunilem8 21224 ordtrest2lem 21808 ptpjpre1 22176 fbfinnfr 22446 filufint 22525 ptcmplem2 22658 cphsqrtcl3 23792 ovoliun 24109 voliunlem3 24156 volsup 24160 cxpsqrt 25294 amgm 25576 wilthlem2 25654 sqff1o 25767 chtublem 25795 bposlem1 25868 bposlem3 25870 ostth 26223 clwwisshclwwslemlem 27798 atdmd 30181 atmd2 30183 mdsymlem4 30189 ordtrest2NEWlem 31275 eulerpartlemb 31736 dfon2lem9 33149 nosupbnd1lem1 33321 nn0prpwlem 33783 bj-ismooredr2 34525 ltflcei 35045 poimirlem30 35087 lplnexllnN 36860 2llnjaN 36862 paddasslem14 37129 cdleme32le 37743 dgrsub2 40079 iccelpart 43950 lighneallem3 44125 lighneal 44129