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 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  sylan  283  vtocl2gf  2885  vtocl3gf  2886  vtoclegft  2897  sbcthdv  3066  disji2  4122  exmid1stab  4345  swopolem  4450  funssres  5420  fvmptssdm  5790  fmptcof  5875  fliftfuns  6004  isorel  6014  oveqrspc2v  6112  caovclg  6242  caovcomg  6245  caovassg  6248  caovcang  6251  caovordig  6255  caovordg  6257  caovdig  6264  caovdirg  6267  qliftfuns  6893  nneneq  7158  supmoti  7333  exmidonfinlem  7545  recexprlemopl  7992  recexprlemopu  7994  cauappcvgprlemladdrl  8024  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsr  8169  suplocsrlempr  8174  ltordlem  8810  lble  9277  uz11  9945  seq3caopr3  10928  hashfibclem  11282  ccatass  11376  swrdswrd  11477  swrdccatin1  11497  swrdccatin2  11501  climcaucn  12117  sumdc  12124  fsum3  12154  fsumf1o  12157  fsum3cvg2  12161  isummulc2  12193  fsum2dlemstep  12201  fisumcom2  12205  fsumshftm  12212  fisum0diag2  12214  fsum00  12229  isumshft  12257  clim2prod  12306  prodmodclem2  12344  zproddc  12346  fprodseq  12350  fprodf1o  12355  prodssdc  12356  fprodm1s  12368  fprodp1s  12369  fprodcllemf  12380  fprodabs  12383  fprod2dlemstep  12389  fprodcom2fi  12393  dvdsprm  12915  pythagtriplem4  13047  pcmptdvds  13124  lidrididd  13702  grpidinv2  13863  ghmlin  14051  srgrz  14288  srglz  14289  ringinvnz1ne0  14354  rrgeq0i  14572  lmodlema  14628  islmodd  14629  lsslss  14718  assalem  15003  ssnei2  15258  psmet0  15428  psmettri2  15429  cncfi  15679  dvcn  15801  dvmptfsum  15826  usgruspgrben  16427  wlk1walkdom  16600  clwwlknonex2lem2  16679  nninfsellemdc  17053