Theorem jaod 725

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

Syntax hints:   → wi 4   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  726  jaao  727  orel2  734  pm2.621  755  mtord  791  jaodan  805  pm2.63  808  pm2.74  815  dedlema  978  dedlemb  979  oplem1  984  ifnebibdc  3655  opthpr  3860  exmid1stab  4304  trsucss  4526  ordsucim  4604  onsucelsucr  4612  0elnn  4723  xpsspw  4844  relop  4886  fununi  5405  poxp  6406  nntri1  6707  nnsseleq  6712  nnmordi  6727  nnaordex  6739  nnm00  6741  swoord2  6775  nneneq  7086  exmidonfinlem  7447  elni2  7577  prubl  7749  distrlem4prl  7847  distrlem4pru  7848  ltxrlt  8287  recexre  8800  remulext1  8821  mulext1  8834  un0addcl  9477  un0mulcl  9478  elnnz  9533  zleloe  9570  zindd  9642  uzsplit  10372  fzm1  10380  expcl2lemap  10859  expnegzap  10881  expaddzap  10891  expmulzap  10893  qsqeqor  10958  nn0opthd  11030  facdiv  11046  facwordi  11048  bcpasc  11074  recvguniq  11618  absexpzap  11703  maxabslemval  11831  xrmaxiflemval  11873  sumrbdclem  12001  summodc  12007  zsumdc  12008  prodrbdclem  12195  zproddc  12203  prodssdc  12213  fprodcl2lem  12229  fprodsplitsn  12257  ordvdsmul  12458  gcdaddm  12618  nninfctlemfo  12674  lcmdvds  12714  dvdsprime  12757  prmdvdsexpr  12785  prmfac1  12787  pythagtriplem2  12902  4sqlem11  13037  unct  13126  domneq0  14351  baspartn  14844  reopnap  15340  coseq0q4123  15628  lgsdir2lem2  15831  upgrpredgv  16070  wlk1walkdom  16283  decidin  16498  bj-charfun  16506  bj-nntrans  16650  bj-nnelirr  16652  bj-findis  16678  triap  16744