Theorem jaod 729

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjaod  730  jaao  731  orel2  738  pm2.621  759  mtord  795  jaodan  809  pm2.63  812  pm2.74  819  dedlema  982  dedlemb  983  oplem1  988  ifnebibdc  3686  opthpr  3897  exmid1stab  4347  trsucss  4570  ordsucim  4649  onsucelsucr  4657  0elnn  4768  xpsspw  4889  relop  4932  fununi  5452  poxp  6472  nntri1  6773  nnsseleq  6778  nnmordi  6793  nnaordex  6805  nnm00  6807  swoord2  6841  nneneq  7162  exmidonfinlem  7551  elni2  7687  prubl  7859  distrlem4prl  7957  distrlem4pru  7958  ltxrlt  8397  recexre  8914  remulext1  8935  mulext1  8948  un0addcl  9607  un0mulcl  9608  elnnz  9665  zleloe  9702  zindd  9775  uzsplit  10516  fzm1  10524  expcl2lemap  11009  expnegzap  11031  expaddzap  11041  expmulzap  11043  qsqeqor  11108  nn0opthd  11182  facdiv  11198  facwordi  11200  bcpasc  11226  recvguniq  11783  absexpzap  11869  maxabslemval  11997  xrmaxiflemval  12041  sumrbdclem  12169  summodc  12175  zsumdc  12176  prodrbdclem  12363  zproddc  12371  prodssdc  12381  fprodcl2lem  12397  fprodsplitsn  12425  ordvdsmul  12626  gcdaddm  12786  nninfctlemfo  12842  lcmdvds  12882  dvdsprime  12925  prmdvdsexpr  12954  prmfac1  12956  pythagtriplem2  13074  4sqlem11  13209  prmlem0  13249  unct  13391  gsummptfidmsplit  14254  domneq0  14690  gsumfsum  15032  baspartn  15276  reopnap  15772  coseq0q4123  16061  rpcxpmul2z  16148  ppiublem1  16291  lgsdir2lem2  16353  upgrpredgv  16592  wlk1walkdom  16805  decidin  17030  bj-charfun  17038  bj-nntrans  17182  bj-nnelirr  17184  bj-findis  17210  triap  17284