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  2834  vtocl3gf  2835  vtoclegft  2844  sbcthdv  3012  disji2  4036  exmid1stab  4251  swopolem  4350  funssres  5310  fvmptssdm  5658  fmptcof  5741  fliftfuns  5857  isorel  5867  oveqrspc2v  5961  caovclg  6089  caovcomg  6092  caovassg  6095  caovcang  6098  caovordig  6102  caovordg  6104  caovdig  6111  caovdirg  6114  qliftfuns  6696  nneneq  6936  supmoti  7077  exmidonfinlem  7283  recexprlemopl  7720  recexprlemopu  7722  cauappcvgprlemladdrl  7752  caucvgsrlemcl  7884  caucvgsrlemfv  7886  caucvgsr  7897  suplocsrlempr  7902  ltordlem  8537  lble  9002  uz11  9653  seq3caopr3  10617  ccatass  11039  climcaucn  11581  sumdc  11588  fsum3  11617  fsumf1o  11620  fsum3cvg2  11624  isummulc2  11656  fsum2dlemstep  11664  fisumcom2  11668  fsumshftm  11675  fisum0diag2  11677  fsum00  11692  isumshft  11720  clim2prod  11769  prodmodclem2  11807  zproddc  11809  fprodseq  11813  fprodf1o  11818  prodssdc  11819  fprodm1s  11831  fprodp1s  11832  fprodcllemf  11843  fprodabs  11846  fprod2dlemstep  11852  fprodcom2fi  11856  dvdsprm  12378  pythagtriplem4  12510  pcmptdvds  12587  lidrididd  13132  grpidinv2  13308  ghmlin  13502  srgrz  13664  srglz  13665  ringinvnz1ne0  13729  rrgeq0i  13944  lmodlema  13972  islmodd  13973  lsslss  14061  ssnei2  14547  psmet0  14717  psmettri2  14718  cncfi  14968  dvcn  15090  dvmptfsum  15115  nninfsellemdc  15811