Theorem jaod 729

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjaod  730  jaao  731  orel2  738  pm2.621  759  mtord  795  jaodan  809  pm2.63  812  pm2.74  819  dedlema  982  dedlemb  983  oplem1  988  ifnebibdc  3686  opthpr  3897  exmid1stab  4345  trsucss  4568  ordsucim  4647  onsucelsucr  4655  0elnn  4766  xpsspw  4887  relop  4930  fununi  5449  poxp  6468  nntri1  6769  nnsseleq  6774  nnmordi  6789  nnaordex  6801  nnm00  6803  swoord2  6837  nneneq  7158  exmidonfinlem  7546  elni2  7682  prubl  7854  distrlem4prl  7952  distrlem4pru  7953  ltxrlt  8392  recexre  8909  remulext1  8930  mulext1  8943  un0addcl  9601  un0mulcl  9602  elnnz  9659  zleloe  9696  zindd  9769  uzsplit  10510  fzm1  10518  expcl2lemap  11003  expnegzap  11025  expaddzap  11035  expmulzap  11037  qsqeqor  11102  nn0opthd  11176  facdiv  11192  facwordi  11194  bcpasc  11220  recvguniq  11777  absexpzap  11863  maxabslemval  11991  xrmaxiflemval  12035  sumrbdclem  12163  summodc  12169  zsumdc  12170  prodrbdclem  12357  zproddc  12365  prodssdc  12375  fprodcl2lem  12391  fprodsplitsn  12419  ordvdsmul  12620  gcdaddm  12780  nninfctlemfo  12836  lcmdvds  12876  dvdsprime  12919  prmdvdsexpr  12948  prmfac1  12950  pythagtriplem2  13068  4sqlem11  13203  prmlem0  13243  unct  13385  domneq0  14665  gsumfsum  15007  baspartn  15242  reopnap  15738  coseq0q4123  16027  ppiublem1  16252  lgsdir2lem2  16314  upgrpredgv  16553  wlk1walkdom  16766  decidin  16991  bj-charfun  16999  bj-nntrans  17143  bj-nnelirr  17145  bj-findis  17171  triap  17244