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  3648  opthpr  3850  exmid1stab  4292  trsucss  4514  ordsucim  4592  onsucelsucr  4600  0elnn  4711  xpsspw  4831  relop  4872  fununi  5389  poxp  6384  nntri1  6650  nnsseleq  6655  nnmordi  6670  nnaordex  6682  nnm00  6684  swoord2  6718  nneneq  7026  exmidonfinlem  7379  elni2  7509  prubl  7681  distrlem4prl  7779  distrlem4pru  7780  ltxrlt  8220  recexre  8733  remulext1  8754  mulext1  8767  un0addcl  9410  un0mulcl  9411  elnnz  9464  zleloe  9501  zindd  9573  uzsplit  10296  fzm1  10304  expcl2lemap  10781  expnegzap  10803  expaddzap  10813  expmulzap  10815  qsqeqor  10880  nn0opthd  10952  facdiv  10968  facwordi  10970  bcpasc  10996  recvguniq  11514  absexpzap  11599  maxabslemval  11727  xrmaxiflemval  11769  sumrbdclem  11896  summodc  11902  zsumdc  11903  prodrbdclem  12090  zproddc  12098  prodssdc  12108  fprodcl2lem  12124  fprodsplitsn  12152  ordvdsmul  12353  gcdaddm  12513  nninfctlemfo  12569  lcmdvds  12609  dvdsprime  12652  prmdvdsexpr  12680  prmfac1  12682  pythagtriplem2  12797  4sqlem11  12932  unct  13021  domneq0  14244  baspartn  14732  reopnap  15228  coseq0q4123  15516  lgsdir2lem2  15716  upgrpredgv  15952  wlk1walkdom  16080  decidin  16185  bj-charfun  16194  bj-nntrans  16338  bj-nnelirr  16340  bj-findis  16366  triap  16427