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  2826  vtocl3gf  2827  vtoclegft  2836  sbcthdv  3004  disji2  4027  exmid1stab  4242  swopolem  4341  funssres  5301  fvmptssdm  5649  fmptcof  5732  fliftfuns  5848  isorel  5858  oveqrspc2v  5952  caovclg  6080  caovcomg  6083  caovassg  6086  caovcang  6089  caovordig  6093  caovordg  6095  caovdig  6102  caovdirg  6105  qliftfuns  6687  nneneq  6927  supmoti  7068  exmidonfinlem  7274  recexprlemopl  7711  recexprlemopu  7713  cauappcvgprlemladdrl  7743  caucvgsrlemcl  7875  caucvgsrlemfv  7877  caucvgsr  7888  suplocsrlempr  7893  ltordlem  8528  lble  8993  uz11  9643  seq3caopr3  10602  climcaucn  11535  sumdc  11542  fsum3  11571  fsumf1o  11574  fsum3cvg2  11578  isummulc2  11610  fsum2dlemstep  11618  fisumcom2  11622  fsumshftm  11629  fisum0diag2  11631  fsum00  11646  isumshft  11674  clim2prod  11723  prodmodclem2  11761  zproddc  11763  fprodseq  11767  fprodf1o  11772  prodssdc  11773  fprodm1s  11785  fprodp1s  11786  fprodcllemf  11797  fprodabs  11800  fprod2dlemstep  11806  fprodcom2fi  11810  dvdsprm  12332  pythagtriplem4  12464  pcmptdvds  12541  lidrididd  13086  grpidinv2  13262  ghmlin  13456  srgrz  13618  srglz  13619  ringinvnz1ne0  13683  rrgeq0i  13898  lmodlema  13926  islmodd  13927  lsslss  14015  ssnei2  14501  psmet0  14671  psmettri2  14672  cncfi  14922  dvcn  15044  dvmptfsum  15069  nninfsellemdc  15765