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  4345  trsucss  4568  ordsucim  4647  onsucelsucr  4655  0elnn  4766  xpsspw  4887  relop  4930  fununi  5449  poxp  6468  nntri1  6769  nnsseleq  6774  nnmordi  6789  nnaordex  6801  nnm00  6803  swoord2  6837  nneneq  7158  exmidonfinlem  7545  elni2  7681  prubl  7853  distrlem4prl  7951  distrlem4pru  7952  ltxrlt  8391  recexre  8906  remulext1  8927  mulext1  8940  un0addcl  9596  un0mulcl  9597  elnnz  9654  zleloe  9691  zindd  9764  uzsplit  10499  fzm1  10507  expcl2lemap  10988  expnegzap  11010  expaddzap  11020  expmulzap  11022  qsqeqor  11087  nn0opthd  11160  facdiv  11176  facwordi  11178  bcpasc  11204  recvguniq  11761  absexpzap  11846  maxabslemval  11974  xrmaxiflemval  12016  sumrbdclem  12144  summodc  12150  zsumdc  12151  prodrbdclem  12338  zproddc  12346  prodssdc  12356  fprodcl2lem  12372  fprodsplitsn  12400  ordvdsmul  12601  gcdaddm  12761  nninfctlemfo  12817  lcmdvds  12857  dvdsprime  12900  prmdvdsexpr  12928  prmfac1  12930  pythagtriplem2  13045  4sqlem11  13180  unct  13333  domneq0  14581  gsumfsum  14923  baspartn  15151  reopnap  15647  coseq0q4123  15935  lgsdir2lem2  16148  upgrpredgv  16387  wlk1walkdom  16600  decidin  16825  bj-charfun  16833  bj-nntrans  16977  bj-nnelirr  16979  bj-findis  17005  triap  17078