Theorem orcd 741

Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)

Hypothesis

Ref	Expression
orcd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
orcd	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Proof of Theorem orcd

Step	Hyp	Ref	Expression
1		orcd.1	. 2 ⊢ (𝜑 → 𝜓)
2		orc 720	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  742  pm2.47  748  orim12i  767  animorl  831  animorrl  834  dcor  944  dfifp2dc  990  undif3ss  3481  dcun  3618  rabsnifsb  3756  exmidn0m  4313  exmidsssn  4314  reg2exmidlema  4655  acexmidlem1  6045  poxp  6427  nntri2or2  6730  nnm00  6762  ssfilem  7129  ssfilemd  7131  diffitest  7143  tridc  7156  finexdc  7159  elssdc  7161  fientri3  7174  unsnfidcex  7179  unsnfidcel  7180  fidcenumlemrks  7222  nninfisollem0  7420  nninfisollemeq  7422  finomni  7430  pr1or2  7490  exmidfodomrlemeldju  7501  exmidfodomrlemreseldju  7502  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  exmidaclem  7514  exmidontriimlem2  7528  netap  7567  2omotaplemap  7570  nqprloc  7859  mullocprlem  7884  recexprlemloc  7945  ltxrlt  8338  zmulcl  9630  nn0lt2  9658  zeo  9682  xrltso  10128  xnn0dcle  10134  xnn0letri  10135  apbtwnz  10633  expnegap0  10908  fzowrddc  11335  xrmaxadd  11942  zsumdc  12066  fsumsplit  12089  sumsplitdc  12114  isumlessdc  12178  zproddc  12261  fprodsplitdc  12278  fprodsplit  12279  fprodunsn  12286  fprodcl2lem  12287  prm23ge5  12958  pcxqcl  13006  gsum0g  13601  lringuplu  14333  aprlring  14426  suplociccreex  15481  lgsdir2lem5  15897  usgredg2v  16211  djulclALT  16565  trilpolemres  16818  trirec0  16820  nconstwlpolem0  16840  nconstwlpolem  16842