Theorem jaod 722

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  723  jaao  724  orel2  731  pm2.621  752  mtord  788  jaodan  802  pm2.63  805  pm2.74  812  dedlema  975  dedlemb  976  oplem1  981  ifnebibdc  3649  opthpr  3853  exmid1stab  4296  trsucss  4518  ordsucim  4596  onsucelsucr  4604  0elnn  4715  xpsspw  4836  relop  4878  fununi  5395  poxp  6392  nntri1  6659  nnsseleq  6664  nnmordi  6679  nnaordex  6691  nnm00  6693  swoord2  6727  nneneq  7038  exmidonfinlem  7394  elni2  7524  prubl  7696  distrlem4prl  7794  distrlem4pru  7795  ltxrlt  8235  recexre  8748  remulext1  8769  mulext1  8782  un0addcl  9425  un0mulcl  9426  elnnz  9479  zleloe  9516  zindd  9588  uzsplit  10317  fzm1  10325  expcl2lemap  10803  expnegzap  10825  expaddzap  10835  expmulzap  10837  qsqeqor  10902  nn0opthd  10974  facdiv  10990  facwordi  10992  bcpasc  11018  recvguniq  11546  absexpzap  11631  maxabslemval  11759  xrmaxiflemval  11801  sumrbdclem  11928  summodc  11934  zsumdc  11935  prodrbdclem  12122  zproddc  12130  prodssdc  12140  fprodcl2lem  12156  fprodsplitsn  12184  ordvdsmul  12385  gcdaddm  12545  nninfctlemfo  12601  lcmdvds  12641  dvdsprime  12684  prmdvdsexpr  12712  prmfac1  12714  pythagtriplem2  12829  4sqlem11  12964  unct  13053  domneq0  14276  baspartn  14764  reopnap  15260  coseq0q4123  15548  lgsdir2lem2  15748  upgrpredgv  15985  wlk1walkdom  16156  decidin  16329  bj-charfun  16338  bj-nntrans  16482  bj-nnelirr  16484  bj-findis  16510  triap  16569