Theorem jaod 689

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)

Hypotheses

Ref	Expression
jaod.1	⊢ (𝜑 → (𝜓 → 𝜒))
jaod.2	⊢ (𝜑 → (𝜃 → 𝜒))

Assertion

Ref	Expression
jaod	⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 30	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 30	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 688	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 30	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 680

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaod  690  jaao  691  orel2  698  pm2.621  719  mtord  755  jaodan  769  pm2.63  772  pm2.74  779  dedlema  936  dedlemb  937  oplem1  942  opthpr  3665  trsucss  4305  ordsucim  4376  onsucelsucr  4384  0elnn  4492  xpsspw  4611  relop  4649  fununi  5149  poxp  6083  nntri1  6346  nnsseleq  6351  nnmordi  6366  nnaordex  6377  nnm00  6379  swoord2  6413  nneneq  6704  elni2  7070  prubl  7242  distrlem4prl  7340  distrlem4pru  7341  ltxrlt  7754  recexre  8258  remulext1  8279  mulext1  8292  un0addcl  8914  un0mulcl  8915  elnnz  8968  zleloe  9005  zindd  9073  uzsplit  9765  fzm1  9773  expcl2lemap  10198  expnegzap  10220  expaddzap  10230  expmulzap  10232  nn0opthd  10361  facdiv  10377  facwordi  10379  bcpasc  10405  recvguniq  10659  absexpzap  10744  maxabslemval  10872  xrmaxiflemval  10911  sumrbdclem  11037  summodc  11044  zsumdc  11045  ordvdsmul  11382  gcdaddm  11520  lcmdvds  11606  dvdsprime  11649  prmdvdsexpr  11674  prmfac1  11676  unct  11797  baspartn  12060  decidin  12696  bj-nntrans  12841  bj-nnelirr  12843  bj-findis  12869  exmid1stab  12887  triap  12916