Theorem jaod 707

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

Syntax hints:   → wi 4   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaod  708  jaao  709  orel2  716  pm2.621  737  mtord  773  jaodan  787  pm2.63  790  pm2.74  797  dedlema  954  dedlemb  955  oplem1  960  opthpr  3731  trsucss  4378  ordsucim  4453  onsucelsucr  4461  0elnn  4572  xpsspw  4691  relop  4729  fununi  5231  poxp  6169  nntri1  6432  nnsseleq  6437  nnmordi  6452  nnaordex  6463  nnm00  6465  swoord2  6499  nneneq  6791  exmidonfinlem  7107  elni2  7213  prubl  7385  distrlem4prl  7483  distrlem4pru  7484  ltxrlt  7922  recexre  8432  remulext1  8453  mulext1  8466  un0addcl  9102  un0mulcl  9103  elnnz  9156  zleloe  9193  zindd  9261  uzsplit  9972  fzm1  9980  expcl2lemap  10409  expnegzap  10431  expaddzap  10441  expmulzap  10443  nn0opthd  10573  facdiv  10589  facwordi  10591  bcpasc  10617  recvguniq  10872  absexpzap  10957  maxabslemval  11085  xrmaxiflemval  11124  sumrbdclem  11251  summodc  11257  zsumdc  11258  prodrbdclem  11445  zproddc  11453  prodssdc  11463  fprodcl2lem  11479  fprodsplitsn  11507  ordvdsmul  11701  gcdaddm  11839  lcmdvds  11927  dvdsprime  11970  prmdvdsexpr  11995  prmfac1  11997  unct  12122  baspartn  12387  reopnap  12877  coseq0q4123  13094  decidin  13309  bj-charfun  13320  bj-nntrans  13464  bj-nnelirr  13466  bj-findis  13492  exmid1stab  13511  triap  13541