Theorem mpan9 281

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	⊢ (𝜑 → 𝜓)
mpan9.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
mpan9	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpan9.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5 32	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 125	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  sylan  283  vtocl2gf  2879  vtocl3gf  2880  vtoclegft  2891  sbcthdv  3060  disji2  4106  exmid1stab  4326  swopolem  4431  funssres  5400  fvmptssdm  5767  fmptcof  5849  fliftfuns  5977  isorel  5987  oveqrspc2v  6085  caovclg  6215  caovcomg  6218  caovassg  6221  caovcang  6224  caovordig  6228  caovordg  6230  caovdig  6237  caovdirg  6240  qliftfuns  6866  nneneq  7124  supmoti  7297  exmidonfinlem  7509  recexprlemopl  7956  recexprlemopu  7958  cauappcvgprlemladdrl  7988  caucvgsrlemcl  8120  caucvgsrlemfv  8122  caucvgsr  8133  suplocsrlempr  8138  ltordlem  8773  lble  9238  uz11  9895  seq3caopr3  10877  hashfibclem  11231  ccatass  11321  swrdswrd  11422  swrdccatin1  11442  swrdccatin2  11446  climcaucn  12061  sumdc  12068  fsum3  12098  fsumf1o  12101  fsum3cvg2  12105  isummulc2  12137  fsum2dlemstep  12145  fisumcom2  12149  fsumshftm  12156  fisum0diag2  12158  fsum00  12173  isumshft  12201  clim2prod  12250  prodmodclem2  12288  zproddc  12290  fprodseq  12294  fprodf1o  12299  prodssdc  12300  fprodm1s  12312  fprodp1s  12313  fprodcllemf  12324  fprodabs  12327  fprod2dlemstep  12333  fprodcom2fi  12337  dvdsprm  12859  pythagtriplem4  12991  pcmptdvds  13068  lidrididd  13645  grpidinv2  13813  ghmlin  14001  srgrz  14227  srglz  14228  ringinvnz1ne0  14292  rrgeq0i  14510  lmodlema  14566  islmodd  14567  lsslss  14655  ssnei2  15148  psmet0  15318  psmettri2  15319  cncfi  15569  dvcn  15691  dvmptfsum  15716  usgruspgrben  16307  wlk1walkdom  16480  clwwlknonex2lem2  16559  nninfsellemdc  16914