Theorem jaod 706

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

Syntax hints:   → wi 4   ∨ wo 697

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 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaod  707  jaao  708  orel2  715  pm2.621  736  mtord  772  jaodan  786  pm2.63  789  pm2.74  796  dedlema  953  dedlemb  954  oplem1  959  opthpr  3699  trsucss  4345  ordsucim  4416  onsucelsucr  4424  0elnn  4532  xpsspw  4651  relop  4689  fununi  5191  poxp  6129  nntri1  6392  nnsseleq  6397  nnmordi  6412  nnaordex  6423  nnm00  6425  swoord2  6459  nneneq  6751  exmidonfinlem  7049  elni2  7122  prubl  7294  distrlem4prl  7392  distrlem4pru  7393  ltxrlt  7830  recexre  8340  remulext1  8361  mulext1  8374  un0addcl  9010  un0mulcl  9011  elnnz  9064  zleloe  9101  zindd  9169  uzsplit  9872  fzm1  9880  expcl2lemap  10305  expnegzap  10327  expaddzap  10337  expmulzap  10339  nn0opthd  10468  facdiv  10484  facwordi  10486  bcpasc  10512  recvguniq  10767  absexpzap  10852  maxabslemval  10980  xrmaxiflemval  11019  sumrbdclem  11146  summodc  11152  zsumdc  11153  prodrbdclem  11340  ordvdsmul  11534  gcdaddm  11672  lcmdvds  11760  dvdsprime  11803  prmdvdsexpr  11828  prmfac1  11830  unct  11954  baspartn  12217  reopnap  12707  coseq0q4123  12915  decidin  13004  bj-nntrans  13149  bj-nnelirr  13151  bj-findis  13177  exmid1stab  13195  triap  13224