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  2885  vtocl3gf  2886  vtoclegft  2897  sbcthdv  3066  disji2  4120  exmid1stab  4343  swopolem  4448  funssres  5418  fvmptssdm  5787  fmptcof  5869  fliftfuns  5997  isorel  6007  oveqrspc2v  6105  caovclg  6235  caovcomg  6238  caovassg  6241  caovcang  6244  caovordig  6248  caovordg  6250  caovdig  6257  caovdirg  6260  qliftfuns  6886  nneneq  7151  supmoti  7326  exmidonfinlem  7538  recexprlemopl  7985  recexprlemopu  7987  cauappcvgprlemladdrl  8017  caucvgsrlemcl  8149  caucvgsrlemfv  8151  caucvgsr  8162  suplocsrlempr  8167  ltordlem  8803  lble  9270  uz11  9927  seq3caopr3  10909  hashfibclem  11263  ccatass  11357  swrdswrd  11458  swrdccatin1  11478  swrdccatin2  11482  climcaucn  12098  sumdc  12105  fsum3  12135  fsumf1o  12138  fsum3cvg2  12142  isummulc2  12174  fsum2dlemstep  12182  fisumcom2  12186  fsumshftm  12193  fisum0diag2  12195  fsum00  12210  isumshft  12238  clim2prod  12287  prodmodclem2  12325  zproddc  12327  fprodseq  12331  fprodf1o  12336  prodssdc  12337  fprodm1s  12349  fprodp1s  12350  fprodcllemf  12361  fprodabs  12364  fprod2dlemstep  12370  fprodcom2fi  12374  dvdsprm  12896  pythagtriplem4  13028  pcmptdvds  13105  lidrididd  13682  grpidinv2  13843  ghmlin  14031  srgrz  14265  srglz  14266  ringinvnz1ne0  14330  rrgeq0i  14548  lmodlema  14604  islmodd  14605  lsslss  14693  ssnei2  15184  psmet0  15354  psmettri2  15355  cncfi  15605  dvcn  15727  dvmptfsum  15752  usgruspgrben  16344  wlk1walkdom  16517  clwwlknonex2lem2  16596  nninfsellemdc  16961