Theorem jaod 724

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

Syntax hints:   → wi 4   ∨ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  725  jaao  726  orel2  733  pm2.621  754  mtord  790  jaodan  804  pm2.63  807  pm2.74  814  dedlema  977  dedlemb  978  oplem1  983  ifnebibdc  3651  opthpr  3855  exmid1stab  4298  trsucss  4520  ordsucim  4598  onsucelsucr  4606  0elnn  4717  xpsspw  4838  relop  4880  fununi  5398  poxp  6397  nntri1  6664  nnsseleq  6669  nnmordi  6684  nnaordex  6696  nnm00  6698  swoord2  6732  nneneq  7043  exmidonfinlem  7404  elni2  7534  prubl  7706  distrlem4prl  7804  distrlem4pru  7805  ltxrlt  8245  recexre  8758  remulext1  8779  mulext1  8792  un0addcl  9435  un0mulcl  9436  elnnz  9489  zleloe  9526  zindd  9598  uzsplit  10327  fzm1  10335  expcl2lemap  10814  expnegzap  10836  expaddzap  10846  expmulzap  10848  qsqeqor  10913  nn0opthd  10985  facdiv  11001  facwordi  11003  bcpasc  11029  recvguniq  11560  absexpzap  11645  maxabslemval  11773  xrmaxiflemval  11815  sumrbdclem  11943  summodc  11949  zsumdc  11950  prodrbdclem  12137  zproddc  12145  prodssdc  12155  fprodcl2lem  12171  fprodsplitsn  12199  ordvdsmul  12400  gcdaddm  12560  nninfctlemfo  12616  lcmdvds  12656  dvdsprime  12699  prmdvdsexpr  12727  prmfac1  12729  pythagtriplem2  12844  4sqlem11  12979  unct  13068  domneq0  14292  baspartn  14780  reopnap  15276  coseq0q4123  15564  lgsdir2lem2  15764  upgrpredgv  16003  wlk1walkdom  16216  decidin  16419  bj-charfun  16428  bj-nntrans  16572  bj-nnelirr  16574  bj-findis  16600  triap  16659