Theorem pm2.21d 622

Description: A contradiction implies anything. Deduction from pm2.21 620. (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 620	. 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 618

This theorem is referenced by:  pm2.21dd  623  pm5.21  699  2falsed  706  mtord  787  prlem1  978  eq0rdv  3516  csbprc  3517  rzal  3569  poirr2  5097  nnsucuniel  6611  nnawordex  6645  swoord2  6680  difinfsnlem  7234  exmidomni  7277  elni2  7469  cauappcvgprlemdisj  7806  caucvgprlemdisj  7829  caucvgprprlemdisj  7857  caucvgsr  7957  lelttr  8203  nnsub  9117  nn0ge2m1nn  9397  elnnz  9424  elnn0z  9427  indstr  9756  indstr2  9772  xrltnsym  9957  xrlttr  9959  xrltso  9960  xrlelttr  9970  xltnegi  9999  xsubge0  10045  ixxdisj  10067  icodisj  10156  fzm1  10264  qbtwnxr  10444  frec2uzlt2d  10593  nn0ltexp2  10898  facdiv  10927  resqrexlemgt0  11497  climuni  11770  fsumcl2lem  11875  dvdsle  12321  prmdvdsexpr  12638  prmfac1  12640  sqrt2irr  12650  phibndlem  12704  dvdsprmpweqle  12826  isxmet2d  14987  lgsdir2lem2  15673  lgseisenlem2  15715  trilpolemres  16321