Theorem ja 188

Description: Inference joining the antecedents of two premises. For partial converses, see jarri 108 and jarli 127. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.)

Hypotheses

Ref	Expression
ja.1	⊢ (¬ 𝜑 → 𝜒)
ja.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
ja	⊢ ((𝜑 → 𝜓) → 𝜒)

Proof of Theorem ja

Step	Hyp	Ref	Expression
1		ja.2	. . 3 ⊢ (𝜓 → 𝜒)
2	1	imim2i 17	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
3		ja.1	. 2 ⊢ (¬ 𝜑 → 𝜒)
4	2, 3	pm2.61d1 182	1 ⊢ ((𝜑 → 𝜓) → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  jad  189  pm2.01  190  peirce  205  oibabs  966  pm2.74  990  pm5.71  1045  meredith  1673  tbw-bijust  1730  tbw-negdf  1731  merco1  1745  19.38  1871  19.35  1909  sbrimvw  2127  sbi2  2335  dfmoeu  2560  moabs  2568  exmoeu  2606  moanimlem  2643  r19.35  3120  r19.21v  3187  elab3gf  3637  elab3g  3638  dfss2  4093  r19.2zb  4455  ralidmw  4471  ralidm  4472  iununi  5058  asymref2  6113  nelaneqOLDOLD  9605  fsuppmapnn0fiub0  14143  itgeq2  26107  frgrwopreglem4a  30920  rmo6  35760  meran1  37323  imsym1  37330  bj-cbvaw  37664  bj-cbveaw  37666  bj-ssbid2ALT  37686  wl-moteq  38583  axc5c7  40105  axc5c711  40112  eu6w  43824  rp-fakeimass  44650  nanorxor  45426  axc5c4c711  45522  pm2.43cbi  45637  euoreqb  48316  oppcendc  50268