Theorem jaod 719

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 718	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 30	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  720  jaao  721  orel2  728  pm2.621  749  mtord  785  jaodan  799  pm2.63  802  pm2.74  809  dedlema  972  dedlemb  973  oplem1  978  ifnebibdc  3619  opthpr  3818  exmid1stab  4259  trsucss  4477  ordsucim  4555  onsucelsucr  4563  0elnn  4674  xpsspw  4794  relop  4835  fununi  5350  poxp  6330  nntri1  6594  nnsseleq  6599  nnmordi  6614  nnaordex  6626  nnm00  6628  swoord2  6662  nneneq  6968  exmidonfinlem  7316  elni2  7442  prubl  7614  distrlem4prl  7712  distrlem4pru  7713  ltxrlt  8153  recexre  8666  remulext1  8687  mulext1  8700  un0addcl  9343  un0mulcl  9344  elnnz  9397  zleloe  9434  zindd  9506  uzsplit  10229  fzm1  10237  expcl2lemap  10713  expnegzap  10735  expaddzap  10745  expmulzap  10747  qsqeqor  10812  nn0opthd  10884  facdiv  10900  facwordi  10902  bcpasc  10928  recvguniq  11376  absexpzap  11461  maxabslemval  11589  xrmaxiflemval  11631  sumrbdclem  11758  summodc  11764  zsumdc  11765  prodrbdclem  11952  zproddc  11960  prodssdc  11970  fprodcl2lem  11986  fprodsplitsn  12014  ordvdsmul  12215  gcdaddm  12375  nninfctlemfo  12431  lcmdvds  12471  dvdsprime  12514  prmdvdsexpr  12542  prmfac1  12544  pythagtriplem2  12659  4sqlem11  12794  unct  12883  domneq0  14104  baspartn  14592  reopnap  15088  coseq0q4123  15376  lgsdir2lem2  15576  decidin  15867  bj-charfun  15877  bj-nntrans  16021  bj-nnelirr  16023  bj-findis  16049  triap  16103