ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jaod GIF version

Theorem jaod 670
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
StepHypRef Expression
1 jaod.1 . . . 4 (𝜑 → (𝜓𝜒))
21com12 30 . . 3 (𝜓 → (𝜑𝜒))
3 jaod.2 . . . 4 (𝜑 → (𝜃𝜒))
43com12 30 . . 3 (𝜃 → (𝜑𝜒))
52, 4jaoi 669 . 2 ((𝜓𝜃) → (𝜑𝜒))
65com12 30 1 (𝜑 → ((𝜓𝜃) → 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpjaod  671  jaao  672  orel2  678  pm2.621  699  mtord  730  jaodan  744  pm2.63  747  pm2.74  754  dedlema  913  dedlemb  914  oplem1  919  opthpr  3599  trsucss  4223  ordsucim  4289  onsucelsucr  4297  0elnn  4404  xpsspw  4517  relop  4553  fununi  5044  poxp  5948  nntri1  6205  nnsseleq  6210  nnmordi  6221  nnaordex  6232  nnm00  6234  swoord2  6268  nneneq  6519  elni2  6810  prubl  6982  distrlem4prl  7080  distrlem4pru  7081  ltxrlt  7489  recexre  7989  remulext1  8010  mulext1  8023  un0addcl  8632  un0mulcl  8633  elnnz  8686  zleloe  8723  zindd  8790  uzsplit  9429  fzm1  9437  expcl2lemap  9858  expnegzap  9880  expaddzap  9890  expmulzap  9892  nn0opthd  10019  facdiv  10035  facwordi  10037  bcpasc  10063  recvguniq  10316  absexpzap  10401  maxabslemval  10529  isumrblem  10648  isummo  10655  zisum  10656  ordvdsmul  10704  gcdaddm  10842  lcmdvds  10928  dvdsprime  10971  prmdvdsexpr  10996  prmfac1  10998  decidin  11127  bj-nntrans  11276  bj-nnelirr  11278  bj-findis  11304
  Copyright terms: Public domain W3C validator