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  6396  nntri1  6663  nnsseleq  6668  nnmordi  6683  nnaordex  6695  nnm00  6697  swoord2  6731  nneneq  7042  exmidonfinlem  7403  elni2  7533  prubl  7705  distrlem4prl  7803  distrlem4pru  7804  ltxrlt  8244  recexre  8757  remulext1  8778  mulext1  8791  un0addcl  9434  un0mulcl  9435  elnnz  9488  zleloe  9525  zindd  9597  uzsplit  10326  fzm1  10334  expcl2lemap  10812  expnegzap  10834  expaddzap  10844  expmulzap  10846  qsqeqor  10911  nn0opthd  10983  facdiv  10999  facwordi  11001  bcpasc  11027  recvguniq  11555  absexpzap  11640  maxabslemval  11768  xrmaxiflemval  11810  sumrbdclem  11937  summodc  11943  zsumdc  11944  prodrbdclem  12131  zproddc  12139  prodssdc  12149  fprodcl2lem  12165  fprodsplitsn  12193  ordvdsmul  12394  gcdaddm  12554  nninfctlemfo  12610  lcmdvds  12650  dvdsprime  12693  prmdvdsexpr  12721  prmfac1  12723  pythagtriplem2  12838  4sqlem11  12973  unct  13062  domneq0  14285  baspartn  14773  reopnap  15269  coseq0q4123  15557  lgsdir2lem2  15757  upgrpredgv  15996  wlk1walkdom  16209  decidin  16393  bj-charfun  16402  bj-nntrans  16546  bj-nnelirr  16548  bj-findis  16574  triap  16633