Theorem pm2.21d 614

Description: A contradiction implies anything. Deduction from pm2.21 612. (Contributed by NM, 10-Feb-1996.)

Hypothesis

Ref	Expression
pm2.21d.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.21d	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem pm2.21d

Step	Hyp	Ref	Expression
1		pm2.21d.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		pm2.21 612	. 2 ⊢ (¬ 𝜓 → (𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 610

This theorem is referenced by:  pm2.21dd  615  pm5.21  690  2falsed  697  mtord  778  prlem1  968  eq0rdv  3459  csbprc  3460  rzal  3512  poirr2  5003  nnsucuniel  6474  nnawordex  6508  swoord2  6543  difinfsnlem  7076  exmidomni  7118  elni2  7276  cauappcvgprlemdisj  7613  caucvgprlemdisj  7636  caucvgprprlemdisj  7664  caucvgsr  7764  lelttr  8008  nnsub  8917  nn0ge2m1nn  9195  elnnz  9222  elnn0z  9225  indstr  9552  indstr2  9568  xrltnsym  9750  xrlttr  9752  xrltso  9753  xrlelttr  9763  xltnegi  9792  xsubge0  9838  ixxdisj  9860  icodisj  9949  fzm1  10056  qbtwnxr  10214  frec2uzlt2d  10360  nn0ltexp2  10644  facdiv  10672  resqrexlemgt0  10984  climuni  11256  fsumcl2lem  11361  dvdsle  11804  prmdvdsexpr  12104  prmfac1  12106  sqrt2irr  12116  phibndlem  12170  dvdsprmpweqle  12290  isxmet2d  13142  lgsdir2lem2  13724  trilpolemres  14074